1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro
  5  
  6  Measurable spaces -- σ-algberas
  7  -/
  8  import data.set.disjointed order.galois_connection data.set.countable
src         └─────────────────┘ └─────────────────────┘ └────────────────┘
  9  
 10  /-!
 11  # Measurable spaces and measurable functions
 12  
 13  This file defines measurable spaces and the functions and isomorphisms
 14  between them.
 15  
 16  A measurable space is a set equipped with a σ-algebra, a collection of
 17  subsets closed under complementation and countable union. A function
 18  between measurable spaces is measurable if the preimage of each
 19  measurable subset is measurable.
 20  
 21  σ-algebras on a fixed set α form a complete lattice. Here we order
 22  σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is
 23  also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any
 24  collection of subsets of α generates a smallest σ-algebra which
 25  contains all of them. A function f : α → β induces a Galois connection
 26  between the lattices of σ-algebras on α and β.
 27  
 28  A measurable equivalence between measurable spaces is an equivalence
 29  which respects the σ-algebras, that is, for which both directions of
 30  the equivalence are measurable functions.
 31  
 32  ## Main statements
 33  
 34  The main theorem of this file is Dynkin's π-λ theorem, which appears
 35  here as an induction principle `induction_on_inter`. Suppose s is a
 36  collection of subsets of α such that the intersection of two members
 37  of s belongs to s whenever it is nonempty. Let m be the σ-algebra
 38  generated by s. In order to check that a predicate C holds on every
 39  member of m, it suffices to check that C holds on the members of s and
 40  that C is preserved by complementation and *disjoint* countable
 41  unions.
 42  
 43  ## Implementation notes
 44  
 45  Measurability of a function f : α → β between measurable spaces is
 46  defined in terms of the Galois connection induced by f.
 47  
 48  ## References
 49  
 50  * <https://en.wikipedia.org/wiki/Measurable_space>
 51  * <https://en.wikipedia.org/wiki/Sigma-algebra>
 52  * <https://en.wikipedia.org/wiki/Dynkin_system>
 53  
 54  ## Tags
 55  
 56  measurable space, measurable function, dynkin system
 57  -/
 58  
 59  local attribute [instance] classical.prop_decidable
id                              └──────────────────────┘
src                             └──────────────────────┘
typ                             └──────────────────────┘
 60  open set lattice encodable
 61  open_locale classical
 62  
 63  universes u v w x
 64  variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort x}
id             
typ            
 65    {s t u : set α}
id              └─┘
src             └─┘
typ             └─┘
 66  
 67  structure measurable_space (α : Type u) :=
id                                   └──┘
typ                                  └──┘
 68  (is_measurable : set α → Prop)
id                    └─┘  
src                   └─┘
typ                   └─┘  
 69  (is_measurable_empty : is_measurable ∅)
id                          └───────────┘ 
src                                       
typ                         └───────────┘ 
 70  (is_measurable_compl : ∀s, is_measurable s → is_measurable (- s))
id                             └───────────┘    └───────────┘   
src                                                              
typ                            └───────────┘    └───────────┘   
 71  (is_measurable_Union : ∀f:ℕ → set α, (∀i, is_measurable (f i)) → is_measurable (⋃i, f i))
id                              └─┘       └───────────┘        └───────────┘    
src                               └─┘                                                
typ                             └─┘       └───────────┘        └───────────┘    
doc                                                                                   
 72  
 73  attribute [class] measurable_space
id                     └──────────────┘
src                    └──────────────┘
typ                    └──────────────┘
 74  
 75  section
 76  variable [measurable_space α]
id             └──────────────┘
src            └──────────────┘
typ            └──────────────┘
 77  
 78  /-- `is_measurable s` means that `s` is measurable (in the ambient measure space on `α`) -/
 79  def is_measurable : set α → Prop := ‹measurable_space α›.is_measurable
id                       └─┘            └──────────────┘ └───────────┘
src                      └─┘             └──────────────┘  └───────────┘
typ                      └─┘            └──────────────┘ └───────────┘
doc                                                        
 80  
 81  lemma is_measurable.empty : is_measurable (∅ : set α) :=
id                               └───────────┘     └─┘ 
src                              └───────────┘     └─┘
typ                              └───────────┘     └─┘ 
doc                              └───────────┘
 82  ‹measurable_space α›.is_measurable_empty
id   └──────────────┘ └─────────────────┘
src  └──────────────┘  └─────────────────┘
typ  └──────────────┘ └─────────────────┘
doc                    
 83  
 84  lemma is_measurable.compl : is_measurable s → is_measurable (-s) :=
id                               └───────────┘    └───────────┘  
src                              └───────────┘     └───────────┘  
typ                              └───────────┘    └───────────┘  
doc                              └───────────┘     └───────────┘
 85  ‹measurable_space α›.is_measurable_compl s
id   └──────────────┘ └─────────────────┘  
src  └──────────────┘  └─────────────────┘
typ  └──────────────┘ └─────────────────┘  
doc                    
 86  
 87  lemma is_measurable.compl_iff : is_measurable (-s) ↔ is_measurable s :=
id                                   └───────────┘     └───────────┘ 
src                                  └───────────┘      └───────────┘
typ                                  └───────────┘     └───────────┘ 
doc                                  └───────────┘        └───────────┘
 88  ⟨λ h, by simpa using h.compl, is_measurable.compl⟩
id                       └─────┘  └─────────────────┘
src           └──────────┘└─────┘  └─────────────────┘
typ          └──────────┘└─────┘  └─────────────────┘
doc           └──────────┘
txt           └──────────┘
par           └──────────┘
pid                └────┘
st           └──────────────────┘
 89  
 90  lemma is_measurable.univ : is_measurable (univ : set α) :=
id                              └───────────┘  └──┘   └─┘ 
src                             └───────────┘  └──┘   └─┘
typ                             └───────────┘  └──┘   └─┘ 
doc                             └───────────┘
 91  by simpa using (@is_measurable.empty α _).compl
id                    └─────────────────┘ 
src     └──────────┘  └─────────────────┘ └─────────
typ     └──────────┘  └─────────────────┘└─────────
doc     └──────────┘                      └─────────
txt     └──────────┘                      └─────────
par     └──────────┘                      └─────────
pid          └────┘                      └──────┘└─
st     └─────────────────────────────────────────────
 92  
src  
typ  
doc  
txt  
par  
pid  
st   
 93  lemma encodable.Union_decode2 {α} [encodable β] (f : β → set α) :
id                                      └───────┘           └─┘ 
src                                     └───────┘             └─┘
typ                                     └───────┘           └─┘ 
doc                                     └───────┘
 94    (⋃ b, f b) = ⋃ (i : ℕ) (b ∈ decode2 β i), f b :=
id                        └─────┘     
src                           └─────┘     
typ                       └─────┘     
doc                                         
 95  ext $ by simp [mem_decode2, exists_swap]
id   └─┘            └─────────┘  └─────────┘
src  └─┘      └────┘└─────────┘└┘└─────────┘└─
typ  └─┘      └────┘└─────────┘└┘└─────────┘└─
doc           └────┘           └┘           └─
txt           └────┘           └┘           └─
par           └────┘           └┘           └─
pid                          └┘           
st           └────────────────────────────────
 96  
src  
typ  
doc  
txt  
par  
pid  
st   
 97  @[elab_as_eliminator] lemma encodable.Union_decode2_cases
doc    └────────────────┘
 98    {α} [encodable β] {f : β → set α} {C : set α → Prop}
id          └───────┘           └─┘        └─┘ 
src         └───────┘             └─┘         └─┘
typ         └───────┘           └─┘        └─┘ 
doc         └───────┘
 99    (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
id                           
src            
typ                          
100    C (⋃ b ∈ decode2 β n, f b) :=
id           └─────┘    
src            └─────┘    
typ          └─────┘    
doc                       
101  match decode2 β n with
id         └─────┘  
src        └─────┘
typ        └─────┘  
102  | none := by simp; apply H0
id     └──┘
src    └──┘       └──┘  └────┘  
typ    └──┘       └──┘  └────┘  
doc               └──┘  └────┘  
txt               └──┘  └────┘  
par               └──┘  └────┘  
pid                            
st               └──────────────┘
103  | (some b) := by convert H1 b; simp [ext_iff]
id      └──┘                  └┘         └─────┘
src     └──┘          └──────┘     └────┘└─────┘└┘
typ     └──┘          └──────┘└┘  └────┘└─────┘└┘
doc                   └──────┘     └────┘       └┘
txt                   └──────┘     └────┘       └┘
par                   └──────┘     └────┘       └┘
pid                                          
st                   └────────────────────────────┘
104  end
105  
106  lemma is_measurable.Union [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
id                              └───────┘           └─┘           └───────────┘   
src                             └───────┘             └─┘             └───────────┘
typ                             └───────┘           └─┘           └───────────┘   
doc                             └───────┘                             └───────────┘
107    is_measurable (⋃b, f b) :=
id     └───────────┘    
src    └───────────┘   
typ    └───────────┘    
doc    └───────────┘   
108  by rw encodable.Union_decode2; exact
id         └─────────────────────┘
src     └─┘└─────────────────────┘  └────┘
typ     └─┘└─────────────────────┘  └────┘
doc     └─┘                         └────┘
txt     └─┘                         └────┘
par     └─┘                         └────┘
pid                                     
st     └──────────────────────────────────
109  ‹measurable_space α›.is_measurable_Union
id   └──────────────┘ 
src  └──────────────┘ └────────────────────
typ  └──────────────┘└────────────────────
doc                   └────────────────────
txt                     └────────────────────
par                     └────────────────────
pid                     └────────────────────
st   ─────────────────────────────────────────
110    (λ n, ⋃ b ∈ decode2 β n, f b)
id                └─────┘    
src  ─┘  └──┘└───┘└─────┘    └─
typ  ─┘  └──┘└───┘└─────┘  └─
doc  ─┘  └──┘└───┘           └─
txt  ─┘  └──┘ └───┘            └─
par  ─┘  └──┘ └───┘            └─
pid  ─┘  └──┘ └───┘            └─
st   ────────────────────────────────
111    (λ n, encodable.Union_decode2_cases is_measurable.empty h)
id           └───────────────────────────┘ └─────────────────┘ 
src  ─┘  └──┘└───────────────────────────┘└─────────────────┘ └─
typ  ─┘  └──┘└───────────────────────────┘└─────────────────┘└─
doc  ─┘  └──┘                                                 └─
txt  ─┘  └──┘                                                 └─
par  ─┘  └──┘                                                 └─
pid  ─┘  └──┘                                                 
st   ─────────────────────────────────────────────────────────────
112  
src  
typ  
doc  
txt  
par  
pid  
st   
113  lemma is_measurable.bUnion {f : β → set α} {s : set β} (hs : countable s)
id                                      └─┘        └─┘         └───────┘ 
src                                      └─┘         └─┘          └───────┘
typ                                     └─┘        └─┘         └───────┘ 
doc                                                               └───────┘
114    (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋃b∈s, f b) :=
id              └───────────┘        └───────────┘     
src              └───────────┘          └───────────┘     
typ             └───────────┘        └───────────┘     
doc               └───────────┘          └───────────┘     
115  begin
st   └─────
116    rw bUnion_eq_Union,
id        └─────────────┘
src    └─┘└─────────────┘
typ    └─┘└─────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────┘└─
117    haveI := hs.to_encodable,
id              └─────────────┘
src    └───────┘└─────────────┘
typ    └───────┘└─────────────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid         └─┘
st   ─────────────────────────┘└─
118    exact is_measurable.Union (by simpa using h)
id           └─────────────────┘                 
src    └────┘└─────────────────┘   └──────────┘ └┘
typ    └────┘└─────────────────┘   └──────────┘└┘
doc    └────┘                      └──────────┘ └┘
txt    └────┘                      └──────────┘ └┘
par    └────┘                      └──────────┘ └┘
pid                               └───────────┘ 
st   ──────────────────────────────┘└────────────┘└┘
119  end
st   └─┘
120  
121  lemma is_measurable.sUnion {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
id                                   └─┘  └─┘          └───────┘            └───────────┘ 
src                                  └─┘  └─┘           └───────┘               └───────────┘
typ                                  └─┘  └─┘          └───────┘            └───────────┘ 
doc                                                     └───────┘               └───────────┘
122    is_measurable (⋃₀ s) :=
id     └───────────┘  └┘ 
src    └───────────┘  └┘
typ    └───────────┘  └┘ 
doc    └───────────┘
123  by rw sUnion_eq_bUnion; exact is_measurable.bUnion hs h
id         └──────────────┘        └──────────────────┘ └┘ 
src     └─┘└──────────────┘  └────┘└──────────────────┘   
typ     └─┘└──────────────┘  └────┘└──────────────────┘└┘
doc     └─┘                  └────┘                       
txt     └─┘                  └────┘                       
par     └─┘                  └────┘                       
pid                                                     
st     └─────────────────────────────────────────────────────
124  
src  
typ  
doc  
txt  
par  
pid  
st   
125  lemma is_measurable.Union_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
id                                                     └─┘            └───────────┘   
src                                                     └─┘              └───────────┘
typ                                                    └─┘            └───────────┘   
doc                                                                      └───────────┘
126    is_measurable (⋃b, f b) :=
id     └───────────┘    
src    └───────────┘   
typ    └───────────┘    
doc    └───────────┘   
127  by by_cases p; simp [h, hf, is_measurable.empty]
id                         └┘  └─────────────────┘
src     └───────┘   └────┘ └┘  └┘└─────────────────┘└─
typ     └───────┘  └────┘└┘└┘└┘└─────────────────┘└─
doc     └───────┘   └────┘ └┘  └┘                   └─
txt     └───────┘   └────┘ └┘  └┘                   └─
par     └───────┘   └────┘ └┘  └┘                   └─
pid                     └┘  └┘                   
st     └──────────────────────────────────────────────
128  
src  
typ  
doc  
txt  
par  
pid  
st   
129  lemma is_measurable.Inter [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
id                              └───────┘           └─┘           └───────────┘   
src                             └───────┘             └─┘             └───────────┘
typ                             └───────┘           └─┘           └───────────┘   
doc                             └───────┘                             └───────────┘
130    is_measurable (⋂b, f b) :=
id     └───────────┘    
src    └───────────┘   
typ    └───────────┘    
doc    └───────────┘   
131  is_measurable.compl_iff.1 $
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
132  by rw compl_Inter; exact is_measurable.Union (λ b, (h b).compl)
id         └─────────┘        └─────────────────┘        
src     └─┘└─────────┘  └────┘└─────────────────┘  └──┘   └────────
typ     └─┘└─────────┘  └────┘└─────────────────┘  └──┘  └────────
doc     └─┘             └────┘                     └──┘   └────────
txt     └─┘             └────┘                     └──┘   └────────
par     └─┘             └────┘                     └──┘   └────────
pid                                              └──┘   └──────┘
st     └─────────────────────────────────────────────────────────────
133  
src  
typ  
doc  
txt  
par  
pid  
st   
134  lemma is_measurable.bInter {f : β → set α} {s : set β} (hs : countable s)
id                                      └─┘        └─┘         └───────┘ 
src                                      └─┘         └─┘          └───────┘
typ                                     └─┘        └─┘         └───────┘ 
doc                                                               └───────┘
135    (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋂b∈s, f b) :=
id              └───────────┘        └───────────┘     
src               └───────────┘          └───────────┘     
typ             └───────────┘        └───────────┘     
doc               └───────────┘          └───────────┘     
136  is_measurable.compl_iff.1 $
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
137  by rw compl_bInter; exact is_measurable.bUnion hs (λ b hb, (h b hb).compl)
id         └──────────┘        └──────────────────┘ └┘           
src     └─┘└──────────┘  └────┘└──────────────────┘    └─────┘     └────────
typ     └─┘└──────────┘  └────┘└──────────────────┘└┘  └─────┘    └────────
doc     └─┘              └────┘                        └─────┘     └────────
txt     └─┘              └────┘                        └─────┘     └────────
par     └─┘              └────┘                        └─────┘     └────────
pid                                                  └─────┘     └──────┘
st     └────────────────────────────────────────────────────────────────────────
138  
src  
typ  
doc  
txt  
par  
pid  
st   
139  lemma is_measurable.sInter {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
id                                   └─┘  └─┘          └───────┘            └───────────┘ 
src                                  └─┘  └─┘           └───────┘               └───────────┘
typ                                  └─┘  └─┘          └───────┘            └───────────┘ 
doc                                                     └───────┘               └───────────┘
140    is_measurable (⋂₀ s) :=
id     └───────────┘  └┘ 
src    └───────────┘  └┘
typ    └───────────┘  └┘ 
doc    └───────────┘  └┘
141  by rw sInter_eq_bInter; exact is_measurable.bInter hs h
id         └──────────────┘        └──────────────────┘ └┘ 
src     └─┘└──────────────┘  └────┘└──────────────────┘   
typ     └─┘└──────────────┘  └────┘└──────────────────┘└┘
doc     └─┘                  └────┘                       
txt     └─┘                  └────┘                       
par     └─┘                  └────┘                       
pid                                                     
st     └─────────────────────────────────────────────────────
142  
src  
typ  
doc  
txt  
par  
pid  
st   
143  lemma is_measurable.Inter_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
id                                                     └─┘            └───────────┘   
src                                                     └─┘              └───────────┘
typ                                                    └─┘            └───────────┘   
doc                                                                      └───────────┘
144    is_measurable (⋂b, f b) :=
id     └───────────┘    
src    └───────────┘   
typ    └───────────┘    
doc    └───────────┘   
145  by by_cases p; simp [h, hf, is_measurable.univ]
id                         └┘  └────────────────┘
src     └───────┘   └────┘ └┘  └┘└────────────────┘└─
typ     └───────┘  └────┘└┘└┘└┘└────────────────┘└─
doc     └───────┘   └────┘ └┘  └┘                  └─
txt     └───────┘   └────┘ └┘  └┘                  └─
par     └───────┘   └────┘ └┘  └┘                  └─
pid                     └┘  └┘                  
st     └─────────────────────────────────────────────
146  
src  
typ  
doc  
txt  
par  
pid  
st   
147  lemma is_measurable.union {s₁ s₂ : set α}
id                                      └─┘ 
src                                     └─┘
typ                                     └─┘ 
148    (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∪ s₂) :=
id           └───────────┘ └┘        └───────────┘ └┘    └───────────┘  └┘  └┘
src          └───────────┘           └───────────┘       └───────────┘     
typ          └───────────┘ └┘        └───────────┘ └┘    └───────────┘  └┘  └┘
doc          └───────────┘           └───────────┘       └───────────┘
149  by rw union_eq_Union; exact
id         └────────────┘
src     └─┘└────────────┘  └────┘
typ     └─┘└────────────┘  └────┘
doc     └─┘                └────┘
txt     └─┘                └────┘
par     └─┘                └────┘
pid                            
st     └─────────────────────────
150  is_measurable.Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
id   └─────────────────┘  └──────────────┘    └┘  └┘
src  └─────────────────┘ └──────────────┘└─┘   └┘  └──
typ  └─────────────────┘ └──────────────┘└─┘ └┘└┘└┘└──
doc                                      └─┘   └┘  └──
txt                                      └─┘   └┘  └──
par                                      └─┘   └┘  └──
pid                                      └─┘   └┘  └┘
st   ──────────────────────────────────────────────────
151  
src  
typ  
doc  
txt  
par  
pid  
st   
152  lemma is_measurable.inter {s₁ s₂ : set α}
id                                      └─┘ 
src                                     └─┘
typ                                     └─┘ 
153    (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∩ s₂) :=
id           └───────────┘ └┘        └───────────┘ └┘    └───────────┘  └┘  └┘
src          └───────────┘           └───────────┘       └───────────┘     
typ          └───────────┘ └┘        └───────────┘ └┘    └───────────┘  └┘  └┘
doc          └───────────┘           └───────────┘       └───────────┘
154  by rw inter_eq_compl_compl_union_compl; exact
id         └──────────────────────────────┘
src     └─┘└──────────────────────────────┘  └────┘
typ     └─┘└──────────────────────────────┘  └────┘
doc     └─┘                                  └────┘
txt     └─┘                                  └────┘
par     └─┘                                  └────┘
pid                                              
st     └───────────────────────────────────────────
155  (h₁.compl.union h₂.compl).compl
id    └────────────┘ └──────┘
src   └────────────┘└──────┘└───────
typ   └────────────┘└──────┘└───────
doc                         └───────
txt                         └───────
par                         └───────
pid                         └────┘└─
st   ────────────────────────────────
156  
src  
typ  
doc  
txt  
par  
pid  
st   
157  lemma is_measurable.diff {s₁ s₂ : set α}
id                                     └─┘ 
src                                    └─┘
typ                                    └─┘ 
158    (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ \ s₂) :=
id           └───────────┘ └┘        └───────────┘ └┘    └───────────┘  └┘  └┘
src          └───────────┘           └───────────┘       └───────────┘     
typ          └───────────┘ └┘        └───────────┘ └┘    └───────────┘  └┘  └┘
doc          └───────────┘           └───────────┘       └───────────┘
159  h₁.inter h₂.compl
id   └┘└────┘ └┘└────┘
src    └────┘   └────┘
typ  └┘└────┘ └┘└────┘
160  
161  lemma is_measurable.sub {s₁ s₂ : set α} :
id                                    └─┘ 
src                                   └─┘
typ                                   └─┘ 
162    is_measurable s₁ → is_measurable s₂ → is_measurable (s₁ - s₂) :=
id     └───────────┘ └┘   └───────────┘ └┘   └───────────┘  └┘  └┘
src    └───────────┘      └───────────┘      └───────────┘     
typ    └───────────┘ └┘   └───────────┘ └┘   └───────────┘  └┘  └┘
doc    └───────────┘      └───────────┘      └───────────┘
163  is_measurable.diff
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
164  
165  lemma is_measurable.disjointed {f : ℕ → set α} (h : ∀i, is_measurable (f i)) (n) :
id                                          └─┘           └───────────┘   
src                                         └─┘             └───────────┘
typ                                         └─┘           └───────────┘   
doc                                                          └───────────┘
166    is_measurable (disjointed f n) :=
id     └───────────┘  └────────┘  
src    └───────────┘  └────────┘
typ    └───────────┘  └────────┘  
doc    └───────────┘  └────────┘
167  disjointed_induct (h n) (assume t i ht, is_measurable.diff ht $ h _)
id   └───────────────┘               └┘  └────────────────┘ └┘   
src  └───────────────┘                       └────────────────┘
typ  └───────────────┘               └┘  └────────────────┘ └┘   
168  
169  lemma is_measurable.const (p : Prop) : is_measurable {a : α | p} :=
id                                          └───────────┘        
src                                         └───────────┘ 
typ                                         └───────────┘        
doc                                         └───────────┘
170  by by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ
id                         └─────────────────┘         └────────────────┘
src     └───────┘   └────┘ └┘└─────────────────┘  └────┘└────────────────┘
typ     └───────┘  └────┘└┘└─────────────────┘  └────┘└────────────────┘
doc     └───────┘   └────┘ └┘                     └────┘                  
txt     └───────┘   └────┘ └┘                     └────┘                  
par     └───────┘   └────┘ └┘                     └────┘                  
pid                     └┘                                            
st     └────────────────────────────────────────────────────────────────────
171  
src  
typ  
doc  
txt  
par  
pid  
st   
172  end
173  
174  @[ext] lemma measurable_space.ext :
doc    └─┘
175    ∀{m₁ m₂ : measurable_space α}, (∀s:set α, m₁.is_measurable s ↔ m₂.is_measurable s) → m₁ = m₂
id              └──────────────┘       └─┘   └┘└────────────┘   └┘└────────────┘     └┘  └┘
src              └──────────────┘         └─┘      └────────────┘      └────────────┘         
typ             └──────────────┘       └─┘   └┘└────────────┘   └┘└────────────┘     └┘  └┘
176  | ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
id      └┘            └┘           
typ     └┘            └┘           
177    have s₁ = s₂, from funext $ assume x, propext $ h x,
id                       └────┘            └─────┘     
src                      └────┘             └─────┘
typ                      └────┘            └─────┘     
178    by subst this
id              └──┘
src       └────┘    
typ       └────┘└──┘
doc       └────┘    
txt       └────┘    
par       └────┘    
pid                
st       └───────────
179  
src  
typ  
doc  
txt  
par  
pid  
st   
180  namespace measurable_space
181  
182  section complete_lattice
183  
184  instance : partial_order (measurable_space α) :=
id              └───────────┘  └──────────────┘ 
src             └───────────┘  └──────────────┘
typ             └───────────┘  └──────────────┘ 
185  { le          := λm₁ m₂, m₁.is_measurable ≤ m₂.is_measurable,
id                    └┘ └┘  └┘└────────────┘  └┘└────────────┘
src                            └────────────┘    └────────────┘
typ                   └┘ └┘  └┘└────────────┘  └┘└────────────┘
186    le_refl     := assume a b, le_refl _,
id                              └─────┘
src                               └─────┘
typ                             └─────┘
187    le_trans    := assume a b c, le_trans,
id                               └──────┘
src                                 └──────┘
typ                              └──────┘
188    le_antisymm := assume a b h₁ h₂, measurable_space.ext $ assume s, ⟨h₁ s, h₂ s⟩ }
id                             └┘ └┘  └──────────────────┘             └┘   └┘ 
src                                     └──────────────────┘
typ                            └┘ └┘  └──────────────────┘             └┘   └┘ 
189  
190  /-- The smallest σ-algebra containing a collection `s` of basic sets -/
191  inductive generate_measurable (s : set (set α)) : set α → Prop
id                                      └─┘  └─┘      └─┘
src                                     └─┘  └─┘       └─┘
typ                                     └─┘  └─┘      └─┘
192  | basic : ∀u∈s, generate_measurable u
id                                      
typ                                     
193  | empty : generate_measurable ∅
id                                 
src                                
typ                                
194  | compl : ∀s, generate_measurable s → generate_measurable (-s)
id                └─────────────────┘                         
src                                                             
typ               └─────────────────┘                         
195  | union : ∀f:ℕ → set α, (∀n, generate_measurable (f n)) → generate_measurable (⋃i, f i)
id                  └─┘                                                          
src                  └─┘                                                            
typ                 └─┘                                                          
doc                                                                                  
196  
197  /-- Construct the smallest measure space containing a collection of basic sets -/
198  def generate_from (s : set (set α)) : measurable_space α :=
id                          └─┘  └─┘      └──────────────┘ 
src                         └─┘  └─┘       └──────────────┘
typ                         └─┘  └─┘      └──────────────┘ 
199  { is_measurable       := generate_measurable s,
id                            └─────────────────┘ 
src                           └─────────────────┘
typ                           └─────────────────┘ 
doc                           └─────────────────┘
200    is_measurable_empty := generate_measurable.empty s,
id                            └───────────────────────┘ 
src                           └───────────────────────┘
typ                           └───────────────────────┘ 
201    is_measurable_compl := generate_measurable.compl,
id                            └───────────────────────┘
src                           └───────────────────────┘
typ                           └───────────────────────┘
202    is_measurable_Union := generate_measurable.union }
id                            └───────────────────────┘
src                           └───────────────────────┘
typ                           └───────────────────────┘
203  
204  lemma is_measurable_generate_from {s : set (set α)} {t : set α} (ht : t ∈ s) :
id                                          └─┘  └─┘         └─┘           
src                                         └─┘  └─┘          └─┘            
typ                                         └─┘  └─┘         └─┘           
205    (generate_from s).is_measurable t :=
id      └───────────┘  └───────────┘  
src     └───────────┘   └───────────┘
typ     └───────────┘  └───────────┘  
doc     └───────────┘
206  generate_measurable.basic t ht
id   └───────────────────────┘  └┘
src  └───────────────────────┘
typ  └───────────────────────┘  └┘
207  
208  lemma generate_from_le {s : set (set α)} {m : measurable_space α} (h : ∀t∈s, m.is_measurable t) :
id                               └─┘  └─┘         └──────────────┘            └────────────┘ 
src                              └─┘  └─┘          └──────────────┘                └────────────┘
typ                              └─┘  └─┘         └──────────────┘            └────────────┘ 
209    generate_from s ≤ m :=
id     └───────────┘   
src    └───────────┘   
typ    └───────────┘   
doc    └───────────┘
210  assume t (ht : generate_measurable s t), ht.rec_on h
id                 └─────────────────┘     └┘└─────┘ 
src                 └─────────────────┘         └─────┘
typ                └─────────────────┘     └┘└─────┘ 
doc                 └─────────────────┘
211    (is_measurable_empty m)
id      └─────────────────┘ 
src     └─────────────────┘
typ     └─────────────────┘ 
212    (assume s _ hs, is_measurable_compl m s hs)
id               └┘  └─────────────────┘   └┘
src                    └─────────────────┘
typ              └┘  └─────────────────┘   └┘
213    (assume f _ hf, is_measurable_Union m f hf)
id               └┘  └─────────────────┘   └┘
src                    └─────────────────┘
typ              └┘  └─────────────────┘   └┘
214  
215  lemma generate_from_le_iff {s : set (set α)} {m : measurable_space α} :
id                                   └─┘  └─┘         └──────────────┘ 
src                                  └─┘  └─┘          └──────────────┘
typ                                  └─┘  └─┘         └──────────────┘ 
216    generate_from s ≤ m ↔ s ⊆ {t | m.is_measurable t} :=
id     └───────────┘          └────────────┘ 
src    └───────────┘               └────────────┘
typ    └───────────┘          └────────────┘ 
doc    └───────────┘
217  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
218    (assume h u hu, h _ $ is_measurable_generate_from hu)
id               └┘       └─────────────────────────┘ └┘
src                          └─────────────────────────┘
typ              └┘       └─────────────────────────┘ └┘
219    (assume h, generate_from_le h)
id               └──────────────┘ 
src               └──────────────┘
typ              └──────────────┘ 
220  
221  protected def mk_of_closure (g : set (set α)) (hg : {t | (generate_from g).is_measurable t} = g) :
id                                    └─┘  └─┘              └───────────┘  └───────────┘     
src                                   └─┘  └─┘                └───────────┘   └───────────┘     
typ                                   └─┘  └─┘              └───────────┘  └───────────┘     
doc                                                            └───────────┘
222    measurable_space α :=
id     └──────────────┘ 
src    └──────────────┘
typ    └──────────────┘ 
223  { is_measurable := λs, s ∈ g,
id                           
src                           
typ                          
224    is_measurable_empty := hg ▸ is_measurable_empty _,
id                            └┘  └─────────────────┘
src                               └─────────────────┘
typ                           └┘  └─────────────────┘
225    is_measurable_compl := hg ▸ is_measurable_compl _,
id                            └┘  └─────────────────┘
src                               └─────────────────┘
typ                           └┘  └─────────────────┘
226    is_measurable_Union := hg ▸ is_measurable_Union _ }
id                            └┘  └─────────────────┘
src                               └─────────────────┘
typ                           └┘  └─────────────────┘
227  
228  lemma mk_of_closure_sets {s : set (set α)}
id                                 └─┘  └─┘ 
src                                └─┘  └─┘
typ                                └─┘  └─┘ 
229    {hs : {t | (generate_from s).is_measurable t} = s} :
id               └───────────┘  └───────────┘     
src               └───────────┘   └───────────┘     
typ              └───────────┘  └───────────┘     
doc                └───────────┘
230    measurable_space.mk_of_closure s hs = generate_from s :=
id     └────────────────────────────┘  └┘  └───────────┘ 
src    └────────────────────────────┘       └───────────┘
typ    └────────────────────────────┘  └┘  └───────────┘ 
doc                                          └───────────┘
231  measurable_space.ext $ assume t, show t ∈ s ↔ _, by rw [← hs] {occs := occurrences.pos [1] }; refl
id   └──────────────────┘                                 └┘           └─────────────┘  
src  └──────────────────┘                              └────┘  └┘ └──────┘└─────────────┘└┘  └────
typ  └──────────────────┘                           └────┘└┘└┘ └──────┘└─────────────┘└┘  └────
doc                                                      └────┘  └┘ └──────┘                 └┘  └────
txt                                                      └────┘  └┘ └──────┘                 └┘  └────
par                                                      └────┘  └┘ └──────┘                 └┘  └────
pid                                                        └──┘   └──────┘                 └┘      
st                                                      └───────┘└─────────────────────────────────────
232  
src  
typ  
doc  
txt  
par  
pid  
st   
233  def gi_generate_from : galois_insertion (@generate_from α) (λm, {t | @is_measurable α m t}) :=
id                          └──────────────┘   └───────────┘           └───────────┘   
src                         └──────────────┘   └───────────┘              └───────────┘
typ                         └──────────────┘   └───────────┘           └───────────┘   
doc                         └──────────────┘   └───────────┘
234  { gc        := assume s m, generate_from_le_iff,
id                            └──────────────────┘
src                             └──────────────────┘
typ                           └──────────────────┘
235    le_l_u    := assume m s, is_measurable_generate_from,
id                            └─────────────────────────┘
src                             └─────────────────────────┘
typ                           └─────────────────────────┘
236    choice    :=
237      λg hg, measurable_space.mk_of_closure g $ le_antisymm hg $ generate_from_le_iff.1 $ le_refl _,
id         └┘  └────────────────────────────┘    └─────────┘ └┘   └──────────────────┘    └─────┘
src             └────────────────────────────┘     └─────────┘      └──────────────────┘    └─────┘
typ        └┘  └────────────────────────────┘    └─────────┘ └┘   └──────────────────┘    └─────┘
238    choice_eq := assume g hg, mk_of_closure_sets }
id                          └┘  └────────────────┘
src                              └────────────────┘
typ                         └┘  └────────────────┘
239  
240  instance : complete_lattice (measurable_space α) :=
id              └──────────────┘  └──────────────┘ 
src             └──────────────┘  └──────────────┘
typ             └──────────────┘  └──────────────┘ 
doc             └──────────────┘
241  gi_generate_from.lift_complete_lattice
id   └──────────────┘└────────────────────┘
src  └──────────────┘└────────────────────┘
typ  └──────────────┘└────────────────────┘
doc                  └────────────────────┘
242  
243  instance : inhabited (measurable_space α) := ⟨⊤⟩
id              └───────┘  └──────────────┘       
src             └───────┘  └──────────────┘        
typ             └───────┘  └──────────────┘       
244  
245  lemma is_measurable_bot_iff {s : set α} : @is_measurable α ⊥ s ↔ (s = ∅ ∨ s = univ) :=
id                                    └─┘      └───────────┘            └──┘
src                                   └─┘       └───────────┘                └──┘
typ                                   └─┘      └───────────┘            └──┘
246  let b : measurable_space α :=
id           └──────────────┘ 
src          └──────────────┘
typ          └──────────────┘ 
247  { is_measurable       := λs, s = ∅ ∨ s = univ,
id                                     └──┘
src                                       └──┘
typ                                    └──┘
248    is_measurable_empty := or.inl rfl,
id                            └────┘ └─┘
src                           └────┘ └─┘
typ                           └────┘ └─┘
249    is_measurable_compl := by simp [or_imp_distrib] {contextual := tt},
id                                     └────────────┘                 └┘
src                              └────┘└────────────┘└┘ └────────────┘└┘
typ                              └────┘└────────────┘└┘ └────────────┘└┘
doc                              └────┘              └┘ └────────────┘  
txt                              └────┘              └┘ └────────────┘  
par                              └────┘              └┘ └────────────┘  
pid                                                 └────────────┘  
st                              └───────────────────────────────────────┘
250    is_measurable_Union := assume f hf, classical.by_cases
id                                    └┘  └────────────────┘
src                                        └────────────────┘
typ                                   └┘  └────────────────┘
251      (assume h : ∃i, f i = univ,
id                       └──┘
src                         └──┘
typ                      └──┘
252        let ⟨i, hi⟩ := h in
id         └─┘    └┘     
typ        └─┘    └┘     
253        or.inr $ eq_univ_of_univ_subset $ hi ▸ le_supr f i)
id         └────┘   └────────────────────┘       └─────┘ 
src        └────┘   └────────────────────┘       └─────┘
typ        └────┘   └────────────────────┘       └─────┘ 
254      (assume h : ¬ ∃i, f i = univ,
id                        └──┘
src                          └──┘
typ                       └──┘
255        or.inl $ eq_empty_of_subset_empty $ Union_subset $ assume i,
id         └────┘   └──────────────────────┘   └──────────┘          
src        └────┘   └──────────────────────┘   └──────────┘
typ        └────┘   └──────────────────────┘   └──────────┘          
256          (hf i).elim (by simp {contextual := tt}) (assume hi, false.elim $ h ⟨i, hi⟩)) } in
id            └┘  └──┘                          └┘           └┘  └────────┘       └┘
src                └──┘      └───┘ └────────────┘└┘              └────────┘
typ           └┘  └──┘      └───┘ └────────────┘└┘          └┘  └────────┘       └┘
doc                          └───┘ └────────────┘  
txt                          └───┘ └────────────┘  
par                          └───┘ └────────────┘  
pid                               └────────────┘  
st                          └──────────────────────┘
257  have b = ⊥, from bot_unique $ assume s hs,
id                 └────────┘           └┘
src                 └────────┘
typ                └────────┘           └┘
258    hs.elim (assume s, s.symm ▸ @is_measurable_empty _ ⊥) (assume s, s.symm ▸ @is_measurable.univ _ ⊥),
id     └┘└───┘           └───┘   └─────────────────┘               └───┘   └────────────────┘   
src      └───┘             └───┘   └─────────────────┘                 └───┘   └────────────────┘   
typ    └┘└───┘           └───┘   └─────────────────┘               └───┘   └────────────────┘   
259  this ▸ iff.rfl
id   └──┘  └─────┘
src        └─────┘
typ  └──┘  └─────┘
260  
261  @[simp] theorem is_measurable_top {s : set α} : @is_measurable _ ⊤ s := trivial
id                                          └─┘      └───────────┘        └─────┘
src                                         └─┘       └───────────┘         └─────┘
typ                                         └─┘      └───────────┘        └─────┘
doc    └──┘
262  
263  @[simp] theorem is_measurable_inf {m₁ m₂ : measurable_space α} {s : set α} :
id                                              └──────────────┘        └─┘ 
src                                             └──────────────┘         └─┘
typ                                             └──────────────┘        └─┘ 
doc    └──┘
264    @is_measurable _ (m₁ ⊓ m₂) s ↔ @is_measurable _ m₁ s ∧ @is_measurable _ m₂ s :=
id      └───────────┘    └┘  └┘     └───────────┘   └┘    └───────────┘   └┘ 
src     └───────────┘                └───────────┘          └───────────┘
typ     └───────────┘    └┘  └┘     └───────────┘   └┘    └───────────┘   └┘ 
265  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
266  
267  @[simp] theorem is_measurable_Inf {ms : set (measurable_space α)} {s : set α} :
id                                           └─┘  └──────────────┘         └─┘ 
src                                          └─┘  └──────────────┘          └─┘
typ                                          └─┘  └──────────────┘         └─┘ 
doc    └──┘
268    @is_measurable _ (Inf ms) s ↔ ∀ m ∈ ms, @is_measurable _ m s :=
id      └───────────┘    └─┘ └┘         └┘   └───────────┘    
src     └───────────┘    └─┘                   └───────────┘
typ     └───────────┘    └─┘ └┘         └┘   └───────────┘    
doc                      └─┘
269  show s ∈ (⋂m∈ms, {t | @is_measurable _ m t }) ↔ _, by simp
id            └┘     └───────────┘        
src                     └───────────┘                 └────
typ           └┘     └───────────┘               └────
doc                                                      └────
txt                                                        └────
par                                                        └────
pid                                                            
st                                                        └─────
270  
src  
typ  
doc  
txt  
par  
pid  
st   
271  @[simp] theorem is_measurable_infi {ι} {m : ι → measurable_space α} {s : set α} :
id                                                  └──────────────┘        └─┘ 
src                                                  └──────────────┘         └─┘
typ                                                 └──────────────┘        └─┘ 
doc    └──┘
272    @is_measurable _ (infi m) s ↔ ∀ i, @is_measurable _ (m i) s :=
id      └───────────┘    └──┘          └───────────┘       
src     └───────────┘    └──┘             └───────────┘
typ     └───────────┘    └──┘          └───────────┘       
doc                      └──┘
273  show s ∈ (λm, {s | @is_measurable _ m s }) (infi m) ↔ _, by rw (@gi_generate_from α).gc.u_infi; simp; refl
id                  └───────────┘         └──┘               └──────────────┘ 
src                    └───────────┘           └──┘           └─┘  └──────────────┘ └─────────┘  └──┘  └────
typ                 └───────────┘         └──┘          └─┘  └──────────────┘└─────────┘  └──┘  └────
doc                                              └──┘            └─┘                   └─────────┘  └──┘  └────
txt                                                              └─┘                   └─────────┘  └──┘  └────
par                                                              └─┘                   └─────────┘  └──┘  └────
pid                                                                                   └────────┘            
st                                                              └───────────────────────────────────────────────
274  
src  
typ  
doc  
txt  
par  
pid  
st   
275  end complete_lattice
276  
277  section functors
278  variables {m m₁ m₂ : measurable_space α} {m' : measurable_space β} {f : α → β} {g : β → α}
id                        └──────────────┘          └──────────────┘
src                       └──────────────┘          └──────────────┘
typ                       └──────────────┘          └──────────────┘
279  
280  /-- The forward image of a measure space under a function. `map f m` contains the sets `s : set β`
281    whose preimage under `f` is measurable. -/
282  protected def map (f : α → β) (m : measurable_space α) : measurable_space β :=
id                                    └──────────────┘     └──────────────┘ 
src                                     └──────────────┘      └──────────────┘
typ                                   └──────────────┘     └──────────────┘ 
283  { is_measurable       := λs, m.is_measurable $ f ⁻¹' s,
id                               └────────────┘    └─┘ 
src                                └────────────┘     └─┘
typ                              └────────────┘    └─┘ 
doc                                                   └─┘
284    is_measurable_empty := m.is_measurable_empty,
id                            └──────────────────┘
src                            └──────────────────┘
typ                           └──────────────────┘
285    is_measurable_compl := assume s hs, m.is_measurable_compl _ hs,
id                                    └┘  └──────────────────┘   └┘
src                                         └──────────────────┘
typ                                   └┘  └──────────────────┘   └┘
286    is_measurable_Union := assume f hf, by rw [preimage_Union]; exact m.is_measurable_Union _ hf }
id                                    └┘         └────────────┘         └───────────────────┘   └┘
src                                           └──┘└────────────┘  └────┘└───────────────────┘└─┘  
typ                                   └┘     └──┘└────────────┘  └────┘└───────────────────┘└─┘└┘
doc                                           └──┘                └────┘                     └─┘  
txt                                           └──┘                └────┘                     └─┘  
par                                           └──┘                └────┘                     └─┘  
pid                                             └┘                                          └─┘  
st                                           └─────────────────┘└─────────────────────────────────┘
287  
288  @[simp] lemma map_id : m.map id = m :=
id                          └──┘ └┘  
src                          └──┘ └┘ 
typ                         └──┘ └┘  
doc    └──┘                  └──┘
289  measurable_space.ext $ assume s, iff.rfl
id   └──────────────────┘            └─────┘
src  └──────────────────┘             └─────┘
typ  └──────────────────┘            └─────┘
290  
291  @[simp] lemma map_comp {f : α → β} {g : β → γ} : (m.map f).map g = m.map (g ∘ f) :=
id                                                 └──┘  └─┘    └──┘    
src                                                     └──┘   └─┘      └──┘    
typ                                                └──┘  └─┘    └──┘    
doc    └──┘                                             └──┘   └─┘       └──┘
292  measurable_space.ext $ assume s, iff.rfl
id   └──────────────────┘            └─────┘
src  └──────────────────┘             └─────┘
typ  └──────────────────┘            └─────┘
293  
294  /-- The reverse image of a measure space under a function. `comap f m` contains the sets `s : set α`
295    such that `s` is the `f`-preimage of a measurable set in `β`. -/
296  protected def comap (f : α → β) (m : measurable_space β) : measurable_space α :=
id                                      └──────────────┘     └──────────────┘ 
src                                       └──────────────┘      └──────────────┘
typ                                     └──────────────┘     └──────────────┘ 
297  { is_measurable       := λs, ∃s', m.is_measurable s' ∧ f ⁻¹' s' = s,
id                               └┘ └────────────┘ └┘   └─┘ └┘  
src                                   └────────────┘       └─┘    
typ                              └┘ └────────────┘ └┘   └─┘ └┘  
doc                                                           └─┘
298    is_measurable_empty := ⟨∅, m.is_measurable_empty, rfl⟩,
id                               └──────────────────┘  └─┘
src                               └──────────────────┘  └─┘
typ                              └──────────────────┘  └─┘
299    is_measurable_compl := assume s ⟨s', h₁, h₂⟩, ⟨-s', m.is_measurable_compl _ h₁, h₂ ▸ rfl⟩,
id                                    └┘  └┘  └┘        └──────────────────┘           └─┘
src                                                        └──────────────────┘           └─┘
typ                                   └┘  └┘  └┘        └──────────────────┘           └─┘
300    is_measurable_Union := assume s hs,
id                                    └┘
typ                                   └┘
301      let ⟨s', hs'⟩ := classical.axiom_of_choice hs in
id       └─┘  └┘  └─┘     └───────────────────────┘ └┘
src                       └───────────────────────┘
typ      └─┘  └┘  └─┘     └───────────────────────┘ └┘
302      ⟨⋃i, s' i, m.is_measurable_Union _ (λi, (hs' i).left), by simp [hs'] ⟩ }
id              └──────────────────┘             └──┘             └─┘
src                └──────────────────┘               └──┘       └────┘   └┘
typ             └──────────────────┘             └──┘       └────┘└─┘└┘
doc                                                              └────┘   └┘
txt                                                                └────┘   └┘
par                                                                └────┘   └┘
pid                                                                       
st                                                                └──────────┘
303  
304  @[simp] lemma comap_id : m.comap id = m :=
id                            └────┘ └┘  
src                            └────┘ └┘ 
typ                           └────┘ └┘  
doc    └──┘                    └────┘
305  measurable_space.ext $ assume s, ⟨assume ⟨s', hs', h⟩, h ▸ hs', assume h, ⟨s, h, rfl⟩⟩
id   └──────────────────┘                        └─┘                           └─┘
src  └──────────────────┘                                                            └─┘
typ  └──────────────────┘                        └─┘                           └─┘
306  
307  @[simp] lemma comap_comp {f : β → α} {g : γ → β} : (m.comap f).comap g = m.comap (f ∘ g) :=
id                                                   └────┘  └───┘    └────┘    
src                                                       └────┘   └───┘      └────┘    
typ                                                  └────┘  └───┘    └────┘    
doc    └──┘                                               └────┘   └───┘       └────┘
308  measurable_space.ext $ assume s,
id   └──────────────────┘          
src  └──────────────────┘
typ  └──────────────────┘          
309    ⟨assume ⟨t, ⟨u, h, hu⟩, ht⟩, ⟨u, h, ht ▸ hu ▸ rfl⟩, assume ⟨t, h, ht⟩, ⟨f ⁻¹' t, ⟨_, h, rfl⟩, ht⟩⟩
id                     └┘   └┘                  └─┘              └┘     └─┘           └─┘
src                                                └─┘                         └─┘           └─┘
typ                    └┘   └┘                  └─┘              └┘     └─┘           └─┘
doc                                                                              └─┘
310  
311  lemma comap_le_iff_le_map {f : α → β} : m'.comap f ≤ m ↔ m' ≤ m.map f :=
id                                         └┘└────┘     └┘  └──┘ 
src                                            └────┘            └──┘
typ                                        └┘└────┘     └┘  └──┘ 
doc                                            └────┘               └──┘
312  ⟨assume h s hs, h _ ⟨_, hs, rfl⟩, assume h s ⟨t, ht, heq⟩, heq ▸ h _ ht⟩
id             └┘         └┘  └─┘               └┘  └─┘        
src                              └─┘                      └─┘       
typ            └┘         └┘  └─┘               └┘  └─┘        
313  
314  lemma gc_comap_map (f : α → β) :
id                              
typ                             
315    galois_connection (measurable_space.comap f) (measurable_space.map f) :=
id     └───────────────┘  └────────────────────┘    └──────────────────┘ 
src    └───────────────┘  └────────────────────┘     └──────────────────┘
typ    └───────────────┘  └────────────────────┘    └──────────────────┘ 
doc    └───────────────┘  └────────────────────┘     └──────────────────┘
316  assume f g, comap_le_iff_le_map
id             └─────────────────┘
src              └─────────────────┘
typ            └─────────────────┘
317  
318  lemma map_mono (h : m₁ ≤ m₂) : m₁.map f ≤ m₂.map f := (gc_comap_map f).monotone_u h
id                       └┘  └┘    └┘└──┘   └┘└──┘      └──────────┘  └────────┘  
src                                  └──┘      └──┘       └──────────┘   └────────┘
typ                      └┘  └┘    └┘└──┘   └┘└──┘      └──────────┘  └────────┘  
doc                                   └──┘       └──┘
319  lemma monotone_map : monotone (measurable_space.map f) := assume a b h, map_mono h
id                        └──────┘  └──────────────────┘                 └──────┘ 
src                       └──────┘  └──────────────────┘                     └──────┘
typ                       └──────┘  └──────────────────┘                 └──────┘ 
doc                       └──────┘  └──────────────────┘
320  lemma comap_mono (h : m₁ ≤ m₂) : m₁.comap g ≤ m₂.comap g := (gc_comap_map g).monotone_l h
id                         └┘  └┘    └┘└────┘   └┘└────┘      └──────────┘  └────────┘  
src                                    └────┘      └────┘       └──────────┘   └────────┘
typ                        └┘  └┘    └┘└────┘   └┘└────┘      └──────────┘  └────────┘  
doc                                     └────┘       └────┘
321  lemma monotone_comap : monotone (measurable_space.comap g) := assume a b h, comap_mono h
id                          └──────┘  └────────────────────┘                 └────────┘ 
src                         └──────┘  └────────────────────┘                     └────────┘
typ                         └──────┘  └────────────────────┘                 └────────┘ 
doc                         └──────┘  └────────────────────┘
322  
323  @[simp] lemma comap_bot : (⊥:measurable_space α).comap g = ⊥ := (gc_comap_map g).l_bot
id                               └──────────────┘  └───┘         └──────────┘  └───┘
src                              └──────────────┘   └───┘          └──────────┘   └───┘
typ                              └──────────────┘  └───┘         └──────────┘  └───┘
doc    └──┘                                          └───┘
324  @[simp] lemma comap_sup : (m₁ ⊔ m₂).comap g = m₁.comap g ⊔ m₂.comap g := (gc_comap_map g).l_sup
id                              └┘  └┘ └───┘    └┘└────┘   └┘└────┘      └──────────┘  └───┘
src                                    └───┘       └────┘      └────┘       └──────────┘   └───┘
typ                             └┘  └┘ └───┘    └┘└────┘   └┘└────┘      └──────────┘  └───┘
doc    └──┘                             └───┘        └────┘       └────┘
325  @[simp] lemma comap_supr {m : ι → measurable_space α} :(⨆i, m i).comap g = (⨆i, (m i).comap g) :=
id                                    └──────────────┘        └───┘         └───┘  
src                                    └──────────────┘            └───┘             └───┘
typ                                   └──────────────┘        └───┘         └───┘  
doc    └──┘                                                        └───┘              └───┘
326  (gc_comap_map g).l_supr
id    └──────────┘  └────┘
src   └──────────┘   └────┘
typ   └──────────┘  └────┘
327  
328  @[simp] lemma map_top : (⊤:measurable_space α).map f = ⊤ := (gc_comap_map f).u_top
id                             └──────────────┘  └─┘         └──────────┘  └───┘
src                            └──────────────┘   └─┘          └──────────┘   └───┘
typ                            └──────────────┘  └─┘         └──────────┘  └───┘
doc    └──┘                                        └─┘
329  @[simp] lemma map_inf : (m₁ ⊓ m₂).map f = m₁.map f ⊓ m₂.map f := (gc_comap_map f).u_inf
id                            └┘  └┘ └─┘    └┘└──┘   └┘└──┘      └──────────┘  └───┘
src                                  └─┘       └──┘      └──┘       └──────────┘   └───┘
typ                           └┘  └┘ └─┘    └┘└──┘   └┘└──┘      └──────────┘  └───┘
doc    └──┘                           └─┘        └──┘       └──┘
330  @[simp] lemma map_infi {m : ι → measurable_space α} : (⨅i, m i).map f = (⨅i, (m i).map f) :=
id                                  └──────────────┘         └─┘         └─┘  
src                                  └──────────────┘             └─┘             └─┘
typ                                 └──────────────┘         └─┘         └─┘  
doc    └──┘                                                       └─┘              └─┘
331  (gc_comap_map f).u_infi
id    └──────────┘  └────┘
src   └──────────┘   └────┘
typ   └──────────┘  └────┘
332  
333  lemma comap_map_le : (m.map f).comap f ≤ m := (gc_comap_map f).l_u_le _
id                         └──┘  └───┘         └──────────┘  └────┘
src                         └──┘   └───┘           └──────────┘   └────┘
typ                        └──┘  └───┘         └──────────┘  └────┘
doc                         └──┘   └───┘
334  lemma le_map_comap : m ≤ (m.comap g).map g := (gc_comap_map g).le_u_l _
id                           └────┘  └─┘       └──────────┘  └────┘
src                            └────┘   └─┘        └──────────┘   └────┘
typ                          └────┘  └─┘       └──────────┘  └────┘
doc                             └────┘   └─┘
335  
336  end functors
337  
338  lemma generate_from_le_generate_from {s t : set (set α)} (h : s ⊆ t) :
id                                               └─┘  └─┘           
src                                              └─┘  └─┘            
typ                                              └─┘  └─┘           
339    generate_from s ≤ generate_from t :=
id     └───────────┘   └───────────┘ 
src    └───────────┘    └───────────┘
typ    └───────────┘   └───────────┘ 
doc    └───────────┘     └───────────┘
340  gi_generate_from.gc.monotone_l h
id   └──────────────┘└─┘└─────────┘ 
src  └──────────────┘└─┘└─────────┘
typ  └──────────────┘└─┘└─────────┘ 
341  
342  lemma generate_from_sup_generate_from {s t : set (set α)} :
id                                                └─┘  └─┘ 
src                                               └─┘  └─┘
typ                                               └─┘  └─┘ 
343    generate_from s ⊔ generate_from t = generate_from (s ∪ t) :=
id     └───────────┘   └───────────┘   └───────────┘    
src    └───────────┘    └───────────┘    └───────────┘    
typ    └───────────┘   └───────────┘   └───────────┘    
doc    └───────────┘     └───────────┘     └───────────┘
344  (@gi_generate_from α).gc.l_sup.symm
id     └──────────────┘  └┘ └───┘ └──┘
src    └──────────────┘   └┘ └───┘ └──┘
typ    └──────────────┘  └┘ └───┘ └──┘
345  
346  lemma comap_generate_from {f : α → β} {s : set (set β)} :
id                                            └─┘  └─┘ 
src                                             └─┘  └─┘
typ                                           └─┘  └─┘ 
347    (generate_from s).comap f = generate_from (preimage f '' s) :=
id      └───────────┘  └───┘    └───────────┘  └──────┘  └┘ 
src     └───────────┘   └───┘     └───────────┘  └──────┘   └┘
typ     └───────────┘  └───┘    └───────────┘  └──────┘  └┘ 
doc     └───────────┘   └───┘      └───────────┘  └──────┘
348  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
349    (comap_le_iff_le_map.2 $ generate_from_le $ assume t hts,
id      └─────────────────┘    └──────────────┘           └─┘
src     └─────────────────┘    └──────────────┘
typ     └─────────────────┘    └──────────────┘           └─┘
350      generate_measurable.basic _ $ mem_image_of_mem _ $ hts)
id       └───────────────────────┘     └──────────────┘     └─┘
src      └───────────────────────┘     └──────────────┘
typ      └───────────────────────┘     └──────────────┘     └─┘
351    (generate_from_le $ assume t ⟨u, hu, eq⟩, eq ▸ ⟨u, generate_measurable.basic _ hu, rfl⟩)
id      └──────────────┘             └┘  └┘           └───────────────────────┘       └─┘
src     └──────────────┘                    └┘           └───────────────────────┘       └─┘
typ     └──────────────┘             └┘  └┘           └───────────────────────┘       └─┘
352  
353  end measurable_space
354  
355  section measurable_functions
356  open measurable_space
357  
358  /-- A function `f` between measurable spaces is measurable if the preimage of every
359    measurable set is measurable. -/
360  def measurable [m₁ : measurable_space α] [m₂ : measurable_space β] (f : α → β) : Prop :=
id                        └──────────────┘         └──────────────┘           
src                       └──────────────┘          └──────────────┘
typ                       └──────────────┘         └──────────────┘           
361  m₂ ≤ m₁.map f
id   └┘  └┘└──┘ 
src        └──┘
typ  └┘  └┘└──┘ 
doc         └──┘
362  
363  lemma measurable_id [measurable_space α] : measurable (@id α) := le_refl _
id                        └──────────────┘     └────────┘   └┘      └─────┘
src                       └──────────────┘      └────────┘   └┘       └─────┘
typ                       └──────────────┘     └────────┘   └┘      └─────┘
doc                                             └────────┘
364  
365  lemma measurable.preimage [measurable_space α] [measurable_space β]
id                              └──────────────┘    └──────────────┘ 
src                             └──────────────┘     └──────────────┘
typ                             └──────────────┘    └──────────────┘ 
366    {f : α → β} (hf : measurable f) {s : set β} : is_measurable s → is_measurable (f ⁻¹' s) := hf _
id                     └────────┘        └─┘     └───────────┘    └───────────┘   └─┘      └┘
src                      └────────┘         └─┘      └───────────┘     └───────────┘    └─┘
typ                    └────────┘        └─┘     └───────────┘    └───────────┘   └─┘      └┘
doc                      └────────┘                  └───────────┘     └───────────┘    └─┘
367  
368  lemma measurable.comp [measurable_space α] [measurable_space β] [measurable_space γ]
id                          └──────────────┘    └──────────────┘    └──────────────┘ 
src                         └──────────────┘     └──────────────┘     └──────────────┘
typ                         └──────────────┘    └──────────────┘    └──────────────┘ 
369    {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) : measurable (g ∘ f) :=
id                               └────────┘         └────────┘     └────────┘    
src                                  └────────┘          └────────┘      └────────┘    
typ                              └────────┘         └────────┘     └────────┘    
doc                                  └────────┘          └────────┘      └────────┘
370  le_trans hg $ map_mono hf
id   └──────┘ └┘   └──────┘ └┘
src  └──────┘      └──────┘
typ  └──────┘ └┘   └──────┘ └┘
371  
372  lemma measurable_generate_from [measurable_space α] {s : set (set β)} {f : α → β}
id                                   └──────────────┘        └─┘  └─┘            
src                                  └──────────────┘         └─┘  └─┘
typ                                  └──────────────┘        └─┘  └─┘            
373    (h : ∀t∈s, is_measurable (f ⁻¹' t)) : @measurable _ _ _ (generate_from s) f :=
id              └───────────┘   └─┘       └────────┘        └───────────┘   
src               └───────────┘    └─┘        └────────┘        └───────────┘
typ             └───────────┘   └─┘       └────────┘        └───────────┘   
doc               └───────────┘    └─┘        └────────┘        └───────────┘
374  generate_from_le h
id   └──────────────┘ 
src  └──────────────┘
typ  └──────────────┘ 
375  
376  lemma measurable.if [measurable_space α] [measurable_space β]
id                        └──────────────┘    └──────────────┘ 
src                       └──────────────┘     └──────────────┘
typ                       └──────────────┘    └──────────────┘ 
377    {p : α → Prop} {h : decidable_pred p} {f g : α → β}
id                        └────────────┘             
src                        └────────────┘
typ                       └────────────┘             
378    (hp : is_measurable {a | p a}) (hf : measurable f) (hg : measurable g) :
id           └───────────┘              └────────┘         └────────┘ 
src          └───────────┘                 └────────┘          └────────┘
typ          └───────────┘              └────────┘         └────────┘ 
doc          └───────────┘                  └────────┘          └────────┘
379    measurable (λa, if p a then f a else g a) :=
id     └────────┘                       
src    └────────┘
typ    └────────┘                       
doc    └────────┘
380  λ s hs, show is_measurable {a | (if p a then f a else g a) ∈ s},
id      └┘       └───────────┘                          
src               └───────────┘                                
typ     └┘       └───────────┘                          
doc               └───────────┘
381  begin
st   └─────
382    convert (hp.inter $ hf s hs).union (hp.compl.inter $ hg s hs),
id              └──────┘   └┘              └────────────┘   └┘  └┘
src    └──────┘ └──────┘      └──────┘ └────────────┘      
typ    └──────┘ └──────┘ └┘   └──────┘ └────────────┘ └┘└┘
doc    └──────┘               └──────┘                     
txt    └──────┘               └──────┘                     
par    └──────┘               └──────┘                     
pid                          └──────┘                     
st   ──────────────────────────────────────────────────────────────┘└─
383    exact ext (λ a, by by_cases p a ; { rw mem_def, simp [h] })
id           └─┘                            └─────┘        
src    └────┘└─┘  └──┘  └───────┘  └──┘└─┘└─────┘└┘└────┘ └┘└─┘
typ    └────┘└─┘  └──┘  └───────┘└──┘└─┘└─────┘└┘└────┘└┘└─┘
doc    └────┘     └──┘  └───────┘  └──┘└─┘       └┘└────┘ └┘└─┘
txt    └────┘     └──┘  └───────┘  └──┘└─┘       └┘└────┘ └┘└─┘
par    └────┘     └──┘  └───────┘  └──┘└─┘       └┘└────┘ └┘└─┘
pid              └──┘  └────────┘  └──────┘       └──────┘ └──┘
st   ───────────────────┘└───────────────┘└─────────┘└─────────┘└┘
384  end
st   └─┘
385  
386  lemma measurable_const {α β} [measurable_space α] [measurable_space β] {a : α} : measurable (λb:β, a) :=
id                                 └──────────────┘    └──────────────┘            └────────┘       
src                                └──────────────┘     └──────────────┘              └────────┘
typ                                └──────────────┘    └──────────────┘            └────────┘       
doc                                                                                   └────────┘
387  assume s hs, show is_measurable {b : β | a ∈ s}, from
id           └┘       └───────────┘          
src                    └───────────┘           
typ          └┘       └───────────┘          
doc                    └───────────┘
388    classical.by_cases
id     └────────────────┘
src    └────────────────┘
typ    └────────────────┘
389      (assume h : a ∈ s, by simp [h]; from is_measurable.univ)
id                                        └────────────────┘
src                           └────┘   └───┘└────────────────┘
typ                         └────┘  └───┘└────────────────┘
doc                            └────┘   └───┘
txt                            └────┘   └───┘
par                            └────┘   └───┘
pid                                   └───┘
st                            └────────────────────────────────┘
390      (assume h : a ∉ s, by simp [h]; from is_measurable.empty)
id                                        └─────────────────┘
src                           └────┘   └───┘└─────────────────┘
typ                         └────┘  └───┘└─────────────────┘
doc                            └────┘   └───┘
txt                            └────┘   └───┘
par                            └────┘   └───┘
pid                                   └───┘
st                            └─────────────────────────────────┘
391  
392  lemma measurable_zero {α β} [measurable_space α] [has_zero α] [measurable_space β] :
id                                └──────────────┘    └──────┘    └──────────────┘ 
src                               └──────────────┘     └──────┘     └──────────────┘
typ                               └──────────────┘    └──────┘    └──────────────┘ 
393    measurable (λb:β, (0:α)) := measurable_const
id     └────────┘                └──────────────┘
src    └────────┘                  └──────────────┘
typ    └────────┘                └──────────────┘
doc    └────────┘
394  
395  end measurable_functions
396  
397  section constructions
398  
399  instance : measurable_space empty := ⊤
id              └──────────────┘ └───┘    
src             └──────────────┘ └───┘    
typ             └──────────────┘ └───┘    
400  instance : measurable_space unit := ⊤
id              └──────────────┘ └──┘    
src             └──────────────┘ └──┘    
typ             └──────────────┘ └──┘    
doc                              └──┘
401  instance : measurable_space bool := ⊤
id              └──────────────┘ └──┘    
src             └──────────────┘ └──┘    
typ             └──────────────┘ └──┘    
402  instance : measurable_space ℕ := ⊤
id              └──────────────┘     
src             └──────────────┘     
typ             └──────────────┘     
403  instance : measurable_space ℤ := ⊤
id              └──────────────┘     
src             └──────────────┘     
typ             └──────────────┘     
404  
405  lemma measurable_unit [measurable_space α] (f : unit → α) : measurable f :=
id                          └──────────────┘        └──┘       └────────┘ 
src                         └──────────────┘         └──┘        └────────┘
typ                         └──────────────┘        └──┘       └────────┘ 
doc                                                  └──┘        └────────┘
406  have f = (λu, f ()) := funext $ assume ⟨⟩, rfl,
id               └┘     └────┘             └─┘
src                 └┘     └────┘             └─┘
typ              └┘     └────┘             └─┘
407  by rw this; exact measurable_const
id         └──┘        └──────────────┘
src     └─┘      └────┘└──────────────┘
typ     └─┘└──┘  └────┘└──────────────┘
doc     └─┘      └────┘                
txt     └─┘      └────┘                
par     └─┘      └────┘                
pid                                  
st     └────────────────────────────────
408  
src  
typ  
doc  
txt  
par  
pid  
st   
409  section nat
410  
411  lemma measurable_from_nat [measurable_space α] {f : ℕ → α} : measurable f :=
id                              └──────────────┘               └────────┘ 
src                             └──────────────┘                 └────────┘
typ                             └──────────────┘               └────────┘ 
doc                                                               └────────┘
412  assume s hs, show is_measurable {n : ℕ | f n ∈ s}, from trivial
id           └┘       └───────────┘                   └─────┘
src                    └───────────┘                      └─────┘
typ          └┘       └───────────┘                   └─────┘
doc                    └───────────┘
413  
414  lemma measurable_to_nat [measurable_space α] {f : α → ℕ} :
id                            └──────────────┘           
src                           └──────────────┘             
typ                           └──────────────┘           
415  (∀ k, is_measurable {x | f x = k}) → measurable f :=
id        └───────────┘            └────────┘ 
src        └───────────┘                └────────┘
typ       └───────────┘            └────────┘ 
doc        └───────────┘                  └────────┘
416  begin
st   └─────
417    assume h s hs, show is_measurable {x | f x ∈ s},
id                         └───────────┘         
src    └───────────┘  └───┘└───────────┘└──┘   
typ    └───────────┘  └───┘└───────────┘└──┘ 
doc    └───────────┘  └───┘└───────────┘ └──┘    
txt    └───────────┘  └───┘              └──┘    
par    └───────────┘  └───┘              └──┘    
pid    └───────────┘  └───┘              └──┘    
st   ──────────────┘└────────────────────────────────┘└─
418    have : {x | f x ∈ s} = ⋃ (n ∈ s), {x | f x = n}, { ext, simp },
id                                       
src    └─────┘ └──┘    └┘└────┘ └──┘        └─┘  └───┘
typ    └─────┘ └──┘    └┘└────┘└──┘       └─┘  └───┘
doc    └─────┘ └──┘    └┘ └────┘  └──┘        └─┘  └───┘
txt    └─────┘ └──┘    └┘  └────┘   └──┘        └─┘  └───┘
par    └─────┘ └──┘    └┘  └────┘   └──┘        └─┘  └───┘
pid    └───┘└┘ └──┘    └┘  └────┘   └──┘                 
st   ────────────────────────────────────────────────┘└──┘└─┘└─────┘└┘
419    rw this, simp [is_measurable.Union, is_measurable.Union_Prop, h]
id        └──┘        └─────────────────┘  └──────────────────────┘  
src    └─┘      └────┘└─────────────────┘└┘└──────────────────────┘└┘ └┘
typ    └─┘└──┘  └────┘└─────────────────┘└┘└──────────────────────┘└┘└┘
doc    └─┘      └────┘                   └┘                        └┘ └┘
txt    └─┘      └────┘                   └┘                        └┘ └┘
par    └─┘      └────┘                   └┘                        └┘ └┘
pid                                   └┘                        └┘ 
st   ────────┘└────────────────────────────────────────────────────────┘
420  end
st   └─┘
421  
422  lemma measurable_find_greatest [measurable_space α] {p : ℕ → α → Prop} :
id                                   └──────────────┘           
src                                  └──────────────┘         
typ                                  └──────────────┘           
423    ∀ {N}, (∀ k ≤ N, is_measurable {x | nat.find_greatest (λ n, p n x) N = k}) →
id                  └───────────┘    └───────────────┘            
src                    └───────────┘     └───────────────┘                
typ                 └───────────┘    └───────────────┘            
doc                     └───────────┘      └───────────────┘
424    measurable (λ x, nat.find_greatest (λ n, p n x) N)
id     └────────┘      └───────────────┘          
src    └────────┘       └───────────────┘
typ    └────────┘      └───────────────┘          
doc    └────────┘       └───────────────┘
425  | 0 := assume h s hs, show is_measurable {x : α | (nat.find_greatest (λ n, p n x) 0) ∈ s},
id                   └┘       └───────────┘         └───────────────┘              
src                             └───────────┘          └───────────────┘                 
typ                  └┘       └───────────┘         └───────────────┘              
doc                             └───────────┘           └───────────────┘
426  begin
st   └─────
427    by_cases h : 0 ∈ s,
id                     
src    └───────┘ └───┘
typ    └───────┘ └───┘
doc    └───────┘ └───┘ 
txt    └───────┘ └───┘ 
par    └───────┘ └───┘ 
pid             └───┘ 
st   ───────────────────┘└─
428    { convert is_measurable.univ, simp only [nat.find_greatest_zero, h] },
id               └────────────────┘             └────────────────────┘  
src      └──────┘└────────────────┘  └─────────┘└────────────────────┘└┘ └┘
typ      └──────┘└────────────────┘  └─────────┘└────────────────────┘└┘└┘
doc      └──────┘                    └─────────┘                      └┘ └┘
txt      └──────┘                    └─────────┘                      └┘ └┘
par      └──────┘                    └─────────┘                      └┘ └┘
pid                                     └──┘└┘                      └┘ 
st   ───┘└────────────────────────┘└──────────────────────────────────────┘└┘
429    { convert is_measurable.empty, simp only [nat.find_greatest_zero, h], refl }
id               └─────────────────┘             └────────────────────┘  
src      └──────┘└─────────────────┘  └─────────┘└────────────────────┘└┘   └───┘
typ      └──────┘└─────────────────┘  └─────────┘└────────────────────┘└┘  └───┘
doc      └──────┘                     └─────────┘                      └┘   └───┘
txt      └──────┘                     └─────────┘                      └┘   └───┘
par      └──────┘                     └─────────┘                      └┘   └───┘
pid                                      └──┘└┘                      └┘       
st   ──────────────────────────────┘└─────────────────────────────────────┘└─────┘└─
430  end
st   ──┘
431  | (n + 1) := assume h,
id                      
src       
typ                     
432  begin
st   └─────
433    apply measurable_to_nat, assume k, by_cases hk : k ≤ n + 1,
id           └───────────────┘                             
src    └────┘└───────────────┘  └──────┘  └───────┘  └─┘  └┘
typ    └────┘└───────────────┘  └──────┘  └───────┘  └─┘└┘
doc    └────┘                   └──────┘  └───────┘  └─┘    └┘
txt    └────┘                   └──────┘  └───────┘  └─┘    └┘
par    └────┘                   └──────┘  └───────┘  └─┘    └┘
pid                            └──────┘            └─┘    
st   ────────────────────────┘└────────┘└───────────────────────┘└─
434    { exact h k hk },
id               └┘
src      └────┘    
typ      └────┘└┘
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───┘└───────────┘└┘
435    { have := is_measurable.empty, rw ← set_of_false at this, convert this, funext, rw eq_false,
id               └─────────────────┘       └──────────┘                  └──┘             └──────┘
src      └──────┘└─────────────────┘  └───┘└──────────┘└──────┘  └──────┘      └────┘  └─┘└──────┘
typ      └──────┘└─────────────────┘  └───┘└──────────┘└──────┘  └──────┘└──┘  └────┘  └─┘└──────┘
doc      └──────┘                     └───┘            └──────┘  └──────┘      └────┘  └─┘
txt      └──────┘                     └───┘            └──────┘  └──────┘      └────┘  └─┘
par      └──────┘                     └───┘            └──────┘  └──────┘      └────┘  └─┘
pid      └───┘└─┘                       └─┘            └──────┘                         
st   ──────────────────────────────┘└─────────────────────────┘└────────────┘└──────┘└───────────┘└─
436      assume h, rw ← h at hk, have := nat.find_greatest_le, contradiction }
id                                      └──────────────────┘
src      └──────┘  └───┘ └────┘  └──────┘└──────────────────┘  └────────────┘
typ      └──────┘  └───┘└────┘  └──────┘└──────────────────┘  └────────────┘
doc      └──────┘  └───┘ └────┘  └──────┘                      └────────────┘
txt      └──────┘  └───┘ └────┘  └──────┘                      └────────────┘
par      └──────┘  └───┘ └────┘  └──────┘                      └────────────┘
pid      └──────┘    └─┘ └────┘  └───┘└─┘                                   
st   ───────────┘└────────────┘└────────────────────────────┘└──────────────┘└─
437  end
st   ──┘
438  
439  end nat
440  
441  section subtype
442  
443  instance {p : α → Prop} [m : measurable_space α] : measurable_space (subtype p) :=
id                               └──────────────┘     └──────────────┘  └─────┘ 
src                               └──────────────┘      └──────────────┘  └─────┘
typ                              └──────────────┘     └──────────────┘  └─────┘ 
444  m.comap subtype.val
id   └────┘ └─────────┘
src   └────┘ └─────────┘
typ  └────┘ └─────────┘
doc   └────┘
445  
446  lemma measurable.subtype_val [measurable_space α] [measurable_space β] {p : β → Prop}
id                                 └──────────────┘    └──────────────┘        
src                                └──────────────┘     └──────────────┘
typ                                └──────────────┘    └──────────────┘        
447    {f : α → subtype p} (hf : measurable f) : measurable (λa:α, (f a).val) :=
id             └─────┘         └────────┘     └────────┘          └─┘
src             └─────┘          └────────┘      └────────┘             └─┘
typ            └─────┘         └────────┘     └────────┘          └─┘
doc                              └────────┘      └────────┘
448  measurable.comp (measurable_space.comap_le_iff_le_map.mp (le_refl _)) hf
id   └─────────────┘  └──────────────────────────────────┘└─┘  └─────┘     └┘
src  └─────────────┘  └──────────────────────────────────┘└─┘  └─────┘
typ  └─────────────┘  └──────────────────────────────────┘└─┘  └─────┘     └┘
449  
450  lemma measurable.subtype_mk [measurable_space α] [measurable_space β] {p : β → Prop}
id                                └──────────────┘    └──────────────┘        
src                               └──────────────┘     └──────────────┘
typ                               └──────────────┘    └──────────────┘        
451    {f : α → subtype p} (hf : measurable (λa, (f a).val)) : measurable f :=
id             └─────┘         └────────┘        └─┘      └────────┘ 
src             └─────┘          └────────┘           └─┘      └────────┘
typ            └─────┘         └────────┘        └─┘      └────────┘ 
doc                              └────────┘                    └────────┘
452  measurable_space.comap_le_iff_le_map.mpr $ by rw [measurable_space.map_comp]; exact hf
id   └──────────────────────────────────┘└──┘          └───────────────────────┘         └┘
src  └──────────────────────────────────┘└──┘      └──┘└───────────────────────┘  └────┘  
typ  └──────────────────────────────────┘└──┘      └──┘└───────────────────────┘  └────┘└┘
doc                                                └──┘                           └────┘  
txt                                                └──┘                           └────┘  
par                                                └──┘                           └────┘  
pid                                                  └┘                                  
st                                                └────────────────────────────┘└──────────
453  
src  
typ  
doc  
txt  
par  
pid  
st   
454  lemma is_measurable_subtype_image [measurable_space α] {s : set α} {t : set s}
id                                      └──────────────┘        └─┘        └─┘ 
src                                     └──────────────┘         └─┘         └─┘
typ                                     └──────────────┘        └─┘        └─┘ 
455    (hs : is_measurable s) : is_measurable t → is_measurable ((coe : s → α) '' t)
id           └───────────┘     └───────────┘   └───────────┘   └─┘        └┘ 
src          └───────────┘      └───────────┘     └───────────┘   └─┘          └┘
typ          └───────────┘     └───────────┘   └───────────┘   └─┘        └┘ 
doc          └───────────┘      └───────────┘     └───────────┘
456  | ⟨u, (hu : is_measurable u), (eq : coe ⁻¹' u = t)⟩ :=
id               └───────────┘           └─┘ └─┘    
src              └───────────┘           └─┘ └─┘   
typ              └───────────┘           └─┘ └─┘    
doc              └───────────┘               └─┘
457    begin
st     └─────
458      rw [← eq, image_preimage_eq_inter_range, range_coe_subtype],
id             └┘  └───────────────────────────┘  └───────────────┘
src      └────┘└┘└┘└───────────────────────────┘└┘└───────────────┘
typ      └────┘└┘└┘└───────────────────────────┘└┘└───────────────┘
doc      └────┘  └┘                             └┘                 
txt      └────┘  └┘                             └┘                 
par      └────┘  └┘                             └┘                 
pid        └──┘  └┘                             └┘                 
st   ───────────┘└─────────────────────────────┘└─────────────────┘└──
459      exact is_measurable.inter hu hs
id             └─────────────────┘ └┘ └┘
src      └────┘└─────────────────┘    
typ      └────┘└─────────────────┘└┘└┘
doc      └────┘                       
txt      └────┘                       
par      └────┘                       
pid                                  
st   ────────────────────────────────────
460    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
461  
462  lemma measurable_of_measurable_union_cover
463    [measurable_space α] [measurable_space β]
id      └──────────────┘    └──────────────┘ 
src     └──────────────┘     └──────────────┘
typ     └──────────────┘    └──────────────┘ 
464    {f : α → β} (s t : set α) (hs : is_measurable s) (ht : is_measurable t) (h : univ ⊆ s ∪ t)
id                      └─┘         └───────────┘         └───────────┘        └──┘    
src                       └─┘          └───────────┘          └───────────┘         └──┘    
typ                     └─┘         └───────────┘         └───────────┘        └──┘    
doc                                    └───────────┘          └───────────┘
465    (hc : measurable (λa:s, f a)) (hd : measurable (λa:t, f a)) :
id           └────────┘                 └────────┘        
src          └────────┘                    └────────┘
typ          └────────┘                 └────────┘        
doc          └────────┘                    └────────┘
466    measurable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
467  assume u (hu : is_measurable u), show is_measurable (f ⁻¹' u), from
id                 └───────────┘         └───────────┘   └─┘ 
src                 └───────────┘          └───────────┘    └─┘
typ                └───────────┘         └───────────┘   └─┘ 
doc                 └───────────┘          └───────────┘    └─┘
468  begin
st   └─────
469    rw show f ⁻¹' u = coe '' (coe ⁻¹' (f ⁻¹' u) : set s) ∪ coe '' (coe ⁻¹' (f ⁻¹' u) : set t),
id               └─┘        └┘                                     └─┘               └─┘ 
src    └─┘     └─┘    └┘             └──┘    └┘      └─┘         └──┘└─┘ └──
typ    └─┘     └─┘    └┘             └──┘   └┘      └─┘       └──┘└─┘└──
doc    └─┘     └─┘                    └──┘    └┘                   └──┘    └──
txt    └─┘                            └──┘    └┘                   └──┘    └──
par    └─┘                            └──┘    └┘                   └──┘    └──
pid                                  └──┘    └┘                   └──┘    └──
st   ─────────────────────────────────────────────────────────────────────────────────────────────
470      by rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, range_coe_subtype, range_coe_subtype, ← inter_distrib_left, univ_subset_iff.1 h, inter_univ],
id              └───────────────────────────┘  └───────────────────────────┘  └───────────────┘  └───────────────┘    └────────────────┘  └─────────────┘     └────────┘
src  ──────────┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────────────┘└┘└───────────────┘└──┘└────────────────┘└┘└─────────────┘└─┘ └┘└────────┘
typ  ──────────┘└───────────────────────────┘└┘└───────────────────────────┘└┘└───────────────┘└┘└───────────────┘└──┘└────────────────┘└┘└─────────────┘└─┘└┘└────────┘
doc  ──────────┘                             └┘                             └┘                 └┘                 └──┘                  └┘               └─┘ └┘          
txt  ──────────┘                             └┘                             └┘                 └┘                 └──┘                  └┘               └─┘ └┘          
par  ──────────┘                             └┘                             └┘                 └┘                 └──┘                  └┘               └─┘ └┘          
pid  ──────────┘                             └┘                             └┘                 └┘                 └──┘                  └┘               └─┘ └┘          
st   ─────┘└────────────────────────────────┘└─────────────────────────────┘└─────────────────┘└─────────────────┘└────────────────────┘└───────────────────┘└──────────┘└─
471    exact is_measurable.union
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ────────────────────────────
472      (is_measurable_subtype_image hs (hc _ hu))
id                                    └┘  └┘
src  ───┘                                 └─┘  └──
typ  ───┘                            └┘ └┘└─┘  └──
doc  ───┘                                 └─┘  └──
txt  ───┘                                 └─┘  └──
par  ───┘                                 └─┘  └──
pid  ───┘                                 └─┘  └──
st   ───────────────────────────────────────────────
473      (is_measurable_subtype_image ht (hd _ hu))
id        └─────────────────────────┘ └┘  └┘   └┘
src  ───┘ └─────────────────────────┘     └─┘  └─┘
typ  ───┘ └─────────────────────────┘└┘ └┘└─┘└┘└─┘
doc  ───┘                                 └─┘  └─┘
txt  ───┘                                 └─┘  └─┘
par  ───┘                                 └─┘  └─┘
pid  ───┘                                 └─┘  └┘
st   ──────────────────────────────────────────────┘
474  end
st   └─┘
475  
476  end subtype
477  
478  section prod
479  
480  instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α × β) :=
id                  └──────────────┘         └──────────────┘     └──────────────┘    
src                 └──────────────┘          └──────────────┘      └──────────────┘    
typ                 └──────────────┘         └──────────────┘     └──────────────┘    
481  m₁.comap prod.fst ⊔ m₂.comap prod.snd
id   └┘└────┘ └──────┘  └┘└────┘ └──────┘
src    └────┘ └──────┘    └────┘ └──────┘
typ  └┘└────┘ └──────┘  └┘└────┘ └──────┘
doc    └────┘              └────┘
482  
483  lemma measurable.fst [measurable_space α] [measurable_space β] [measurable_space γ]
id                         └──────────────┘    └──────────────┘    └──────────────┘ 
src                        └──────────────┘     └──────────────┘     └──────────────┘
typ                        └──────────────┘    └──────────────┘    └──────────────┘ 
484    {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).1) :=
id                       └────────┘     └────────┘          
src                         └────────┘      └────────┘             
typ                      └────────┘     └────────┘          
doc                          └────────┘      └────────┘
485  measurable.comp (measurable_space.comap_le_iff_le_map.mp le_sup_left) hf
id   └─────────────┘  └──────────────────────────────────┘└─┘ └─────────┘  └┘
src  └─────────────┘  └──────────────────────────────────┘└─┘ └─────────┘
typ  └─────────────┘  └──────────────────────────────────┘└─┘ └─────────┘  └┘
486  
487  lemma measurable.snd [measurable_space α] [measurable_space β] [measurable_space γ]
id                         └──────────────┘    └──────────────┘    └──────────────┘ 
src                        └──────────────┘     └──────────────┘     └──────────────┘
typ                        └──────────────┘    └──────────────┘    └──────────────┘ 
488    {f : α → β × γ} (hf : measurable f) : measurable (λa:α, (f a).2) :=
id                       └────────┘     └────────┘          
src                         └────────┘      └────────┘             
typ                      └────────┘     └────────┘          
doc                          └────────┘      └────────┘
489  measurable.comp (measurable_space.comap_le_iff_le_map.mp le_sup_right) hf
id   └─────────────┘  └──────────────────────────────────┘└─┘ └──────────┘  └┘
src  └─────────────┘  └──────────────────────────────────┘└─┘ └──────────┘
typ  └─────────────┘  └──────────────────────────────────┘└─┘ └──────────┘  └┘
490  
491  lemma measurable.prod [measurable_space α] [measurable_space β] [measurable_space γ]
id                          └──────────────┘    └──────────────┘    └──────────────┘ 
src                         └──────────────┘     └──────────────┘     └──────────────┘
typ                         └──────────────┘    └──────────────┘    └──────────────┘ 
492    {f : α → β × γ} (hf₁ : measurable (λa, (f a).1)) (hf₂ : measurable (λa, (f a).2)) :
id                        └────────┘                   └────────┘        
src                          └────────┘                      └────────┘           
typ                       └────────┘                   └────────┘        
doc                           └────────┘                       └────────┘
493    measurable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
494  sup_le
id   └────┘
src  └────┘
typ  └────┘
495    (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₁)
id             └──────────────────────────────────┘  └───────────────────────┘         └─┘
src        └──┘└──────────────────────────────────┘└┘└───────────────────────┘  └────┘
typ        └──┘└──────────────────────────────────┘└┘└───────────────────────┘  └────┘└─┘
doc        └──┘                                    └┘                           └────┘
txt        └──┘                                    └┘                           └────┘
par        └──┘                                    └┘                           └────┘
pid          └┘                                    └┘                                
st        └───────────────────────────────────────┘└─────────────────────────┘└─────────┘
496    (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₂)
id             └──────────────────────────────────┘  └───────────────────────┘         └─┘
src        └──┘└──────────────────────────────────┘└┘└───────────────────────┘  └────┘
typ        └──┘└──────────────────────────────────┘└┘└───────────────────────┘  └────┘└─┘
doc        └──┘                                    └┘                           └────┘
txt        └──┘                                    └┘                           └────┘
par        └──┘                                    └┘                           └────┘
pid          └┘                                    └┘                                
st        └───────────────────────────────────────┘└─────────────────────────┘└─────────┘
497  
498  lemma measurable.prod_mk [measurable_space α] [measurable_space β] [measurable_space γ]
id                             └──────────────┘    └──────────────┘    └──────────────┘ 
src                            └──────────────┘     └──────────────┘     └──────────────┘
typ                            └──────────────┘    └──────────────┘    └──────────────┘ 
499    {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : measurable (λa:α, (f a, g a)) :=
id                               └────────┘         └────────┘     └────────┘           
src                                  └────────┘          └────────┘      └────────┘        
typ                              └────────┘         └────────┘     └────────┘           
doc                                  └────────┘          └────────┘      └────────┘
500  measurable.prod hf hg
id   └─────────────┘ └┘ └┘
src  └─────────────┘
typ  └─────────────┘ └┘ └┘
501  
502  lemma is_measurable_set_prod [measurable_space α] [measurable_space β] {s : set α} {t : set β}
id                                 └──────────────┘    └──────────────┘        └─┘        └─┘ 
src                                └──────────────┘     └──────────────┘         └─┘         └─┘
typ                                └──────────────┘    └──────────────┘        └─┘        └─┘ 
503    (hs : is_measurable s) (ht : is_measurable t) : is_measurable (set.prod s t) :=
id           └───────────┘         └───────────┘     └───────────┘  └──────┘  
src          └───────────┘          └───────────┘      └───────────┘  └──────┘
typ          └───────────┘         └───────────┘     └───────────┘  └──────┘  
doc          └───────────┘          └───────────┘      └───────────┘  └──────┘
504  is_measurable.inter (measurable.fst measurable_id _ hs) (measurable.snd measurable_id _ ht)
id   └─────────────────┘  └────────────┘ └───────────┘   └┘   └────────────┘ └───────────┘   └┘
src  └─────────────────┘  └────────────┘ └───────────┘        └────────────┘ └───────────┘
typ  └─────────────────┘  └────────────┘ └───────────┘   └┘   └────────────┘ └───────────┘   └┘
505  
506  end prod
507  
508  section pi
509  
510  instance measurable_space.pi {α : Type u} {β : α → Type v} [m : Πa, measurable_space (β a)] :
id                                                                     └──────────────┘   
src                                                                      └──────────────┘
typ                                                                    └──────────────┘   
511    measurable_space (Πa, β a) :=
id     └──────────────┘      
src    └──────────────┘
typ    └──────────────┘      
512  ⨆a, (m a).comap (λb, b a)
id       └───┘       
src         └───┘
typ      └───┘       
doc         └───┘
513  
514  lemma measurable_pi_apply {α : Type u} {β : α → Type v} [Πa, measurable_space (β a)] (a : α) :
id                                                              └──────────────┘           
src                                                               └──────────────┘
typ                                                             └──────────────┘           
515    measurable (λf:Πa, β a, f a) :=
id     └────────┘            
src    └────────┘
typ    └────────┘            
doc    └────────┘
516  measurable_space.comap_le_iff_le_map.1 $ lattice.le_supr _ a
id   └──────────────────────────────────┘    └─────────────┘   
src  └──────────────────────────────────┘    └─────────────┘
typ  └──────────────────────────────────┘    └─────────────┘   
517  
518  lemma measurable_pi_lambda {α : Type u} {β : α → Type v} {γ : Type w}
id                                                
typ                                               
519    [Πa, measurable_space (β a)] [measurable_space γ]
id         └──────────────┘       └──────────────┘ 
src         └──────────────┘         └──────────────┘
typ        └──────────────┘       └──────────────┘ 
520    (f : γ → Πa, β a) (hf : ∀a, measurable (λc, f c a)) :
id                            └────────┘       
src                                └────────┘
typ                           └────────┘       
doc                                └────────┘
521    measurable f :=
id     └────────┘ 
src    └────────┘
typ    └────────┘ 
doc    └────────┘
522  lattice.supr_le $ assume a, measurable_space.comap_le_iff_le_map.2 (hf a)
id   └─────────────┘            └──────────────────────────────────┘   └┘ 
src  └─────────────┘             └──────────────────────────────────┘
typ  └─────────────┘            └──────────────────────────────────┘   └┘ 
523  
524  end pi
525  
526  instance [m₁ : measurable_space α] [m₂ : measurable_space β] : measurable_space (α ⊕ β) :=
id                  └──────────────┘         └──────────────┘     └──────────────┘    
src                 └──────────────┘          └──────────────┘      └──────────────┘    
typ                 └──────────────┘         └──────────────┘     └──────────────┘    
527  m₁.map sum.inl ⊓ m₂.map sum.inr
id   └┘└──┘ └─────┘  └┘└──┘ └─────┘
src    └──┘ └─────┘    └──┘ └─────┘
typ  └┘└──┘ └─────┘  └┘└──┘ └─────┘
doc    └──┘             └──┘
528  
529  section sum
530  variables [measurable_space α] [measurable_space β] [measurable_space γ]
id              └──────────────┘     └──────────────┘     └──────────────┘
src             └──────────────┘     └──────────────┘     └──────────────┘
typ             └──────────────┘     └──────────────┘     └──────────────┘
531  
532  lemma measurable_inl : measurable (@sum.inl α β) := inf_le_left
id                          └────────┘   └─────┘       └─────────┘
src                         └────────┘   └─────┘         └─────────┘
typ                         └────────┘   └─────┘       └─────────┘
doc                         └────────┘
533  
534  lemma measurable_inr : measurable (@sum.inr α β) := inf_le_right
id                          └────────┘   └─────┘       └──────────┘
src                         └────────┘   └─────┘         └──────────┘
typ                         └────────┘   └─────┘       └──────────┘
doc                         └────────┘
535  
536  lemma measurable_sum {f : α ⊕ β → γ}
id                                  
src                              
typ                                 
537    (hl : measurable (f ∘ sum.inl)) (hr : measurable (f ∘ sum.inr)) : measurable f :=
id           └────────┘    └─────┘         └────────┘    └─────┘     └────────┘ 
src          └────────┘     └─────┘         └────────┘     └─────┘     └────────┘
typ          └────────┘    └─────┘         └────────┘    └─────┘     └────────┘ 
doc          └────────┘                      └────────┘                  └────────┘
538  measurable_space.comap_le_iff_le_map.1 $ le_inf
id   └──────────────────────────────────┘    └────┘
src  └──────────────────────────────────┘    └────┘
typ  └──────────────────────────────────┘    └────┘
539    (measurable_space.comap_le_iff_le_map.2 $ hl)
id      └──────────────────────────────────┘    └┘
src     └──────────────────────────────────┘
typ     └──────────────────────────────────┘    └┘
540    (measurable_space.comap_le_iff_le_map.2 $ hr)
id      └──────────────────────────────────┘    └┘
src     └──────────────────────────────────┘
typ     └──────────────────────────────────┘    └┘
541  
542  lemma measurable_sum_rec {f : α → γ} {g : β → γ}
id                                              
typ                                             
543    (hf : measurable f) (hg : measurable g) : @measurable (α ⊕ β) γ _ _ (@sum.rec α β (λ_, γ) f g) :=
id           └────────┘         └────────┘      └────────┘             └─────┘          
src          └────────┘          └────────┘       └────────┘                └─────┘
typ          └────────┘         └────────┘      └────────┘             └─────┘          
doc          └────────┘          └────────┘       └────────┘
544  measurable_sum hf hg
id   └────────────┘ └┘ └┘
src  └────────────┘
typ  └────────────┘ └┘ └┘
545  
546  lemma is_measurable_inl_image {s : set α} (hs : is_measurable s) :
id                                      └─┘         └───────────┘ 
src                                     └─┘          └───────────┘
typ                                     └─┘         └───────────┘ 
doc                                                  └───────────┘
547    is_measurable (sum.inl '' s : set (α ⊕ β)) :=
id     └───────────┘  └─────┘ └┘    └─┘    
src    └───────────┘  └─────┘ └┘     └─┘    
typ    └───────────┘  └─────┘ └┘    └─┘    
doc    └───────────┘
548  ⟨show is_measurable (sum.inl ⁻¹' _), by rwa [preimage_image_eq]; exact (assume a b, sum.inl.inj),
id         └───────────┘  └─────┘ └─┘             └───────────────┘                      └─────────┘
src        └───────────┘  └─────┘ └─┘        └───┘└───────────────┘  └────┘       └────┘└─────────┘
typ        └───────────┘  └─────┘ └─┘        └───┘└───────────────┘  └────┘       └────┘└─────────┘
doc        └───────────┘          └─┘        └───┘                   └────┘       └────┘           
txt                                          └───┘                   └────┘       └────┘           
par                                          └───┘                   └────┘       └────┘           
pid                                             └┘                               └────┘           
st                                          └─────────────────────┘└───────────────────────────────┘
549    have sum.inr ⁻¹' (sum.inl '' s : set (α ⊕ β)) = ∅ :=
id          └─────┘ └─┘  └─────┘ └┘    └─┘        
src         └─────┘ └─┘  └─────┘ └┘     └─┘          
typ         └─────┘ └─┘  └─────┘ └┘    └─┘        
doc                 └─┘
550      eq_empty_of_subset_empty $ assume x ⟨y, hy, eq⟩, by contradiction,
id       └──────────────────────┘           
src      └──────────────────────┘                            └───────────┘
typ      └──────────────────────┘                          └───────────┘
doc                                                          └───────────┘
txt                                                          └───────────┘
par                                                          └───────────┘
st                                                          └────────────┘
551    show is_measurable (sum.inr ⁻¹' _), by rw [this]; exact is_measurable.empty⟩
id          └───────────┘  └─────┘ └─┘            └──┘         └─────────────────┘
src         └───────────┘  └─────┘ └─┘        └──┘      └────┘└─────────────────┘
typ         └───────────┘  └─────┘ └─┘        └──┘└──┘  └────┘└─────────────────┘
doc         └───────────┘          └─┘        └──┘      └────┘
txt                                           └──┘      └────┘
par                                           └──┘      └────┘
pid                                             └┘           
st                                           └───────┘└─────────────────────────┘
552  
553  lemma is_measurable_range_inl : is_measurable (range sum.inl : set (α ⊕ β)) :=
id                                   └───────────┘  └───┘ └─────┘   └─┘    
src                                  └───────────┘  └───┘ └─────┘   └─┘    
typ                                  └───────────┘  └───┘ └─────┘   └─┘    
doc                                  └───────────┘  └───┘
554  by rw [← image_univ]; exact is_measurable_inl_image is_measurable.univ
id            └────────┘         └─────────────────────┘ └────────────────┘
src     └────┘└────────┘  └────┘└─────────────────────┘└────────────────┘
typ     └────┘└────────┘  └────┘└─────────────────────┘└────────────────┘
doc     └────┘            └────┘                                         
txt     └────┘            └────┘                                         
par     └────┘            └────┘                                         
pid       └──┘                                                          
st     └───────────────┘└──────────────────────────────────────────────────
555  
src  
typ  
doc  
txt  
par  
pid  
st   
556  lemma is_measurable_inr_image {s : set β} (hs : is_measurable s) :
id                                      └─┘         └───────────┘ 
src                                     └─┘          └───────────┘
typ                                     └─┘         └───────────┘ 
doc                                                  └───────────┘
557    is_measurable (sum.inr '' s : set (α ⊕ β)) :=
id     └───────────┘  └─────┘ └┘    └─┘    
src    └───────────┘  └─────┘ └┘     └─┘    
typ    └───────────┘  └─────┘ └┘    └─┘    
doc    └───────────┘
558  ⟨ have sum.inl ⁻¹' (sum.inr '' s : set (α ⊕ β)) = ∅ :=
id          └─────┘ └─┘  └─────┘ └┘    └─┘        
src         └─────┘ └─┘  └─────┘ └┘     └─┘          
typ         └─────┘ └─┘  └─────┘ └┘    └─┘        
doc                 └─┘
559      eq_empty_of_subset_empty $ assume x ⟨y, hy, eq⟩, by contradiction,
id       └──────────────────────┘           
src      └──────────────────────┘                            └───────────┘
typ      └──────────────────────┘                          └───────────┘
doc                                                          └───────────┘
txt                                                          └───────────┘
par                                                          └───────────┘
st                                                          └────────────┘
560    show is_measurable (sum.inl ⁻¹' _), by rw [this]; exact is_measurable.empty,
id          └───────────┘  └─────┘ └─┘            └──┘         └─────────────────┘
src         └───────────┘  └─────┘ └─┘        └──┘      └────┘└─────────────────┘
typ         └───────────┘  └─────┘ └─┘        └──┘└──┘  └────┘└─────────────────┘
doc         └───────────┘          └─┘        └──┘      └────┘
txt                                           └──┘      └────┘
par                                           └──┘      └────┘
pid                                             └┘           
st                                           └───────┘└─────────────────────────┘
561    show is_measurable (sum.inr ⁻¹' _), by rwa [preimage_image_eq]; exact (assume a b, sum.inr.inj)⟩
id          └───────────┘  └─────┘ └─┘             └───────────────┘                      └─────────┘
src         └───────────┘  └─────┘ └─┘        └───┘└───────────────┘  └────┘       └────┘└─────────┘
typ         └───────────┘  └─────┘ └─┘        └───┘└───────────────┘  └────┘       └────┘└─────────┘
doc         └───────────┘          └─┘        └───┘                   └────┘       └────┘           
txt                                           └───┘                   └────┘       └────┘           
par                                           └───┘                   └────┘       └────┘           
pid                                              └┘                               └────┘           
st                                           └─────────────────────┘└───────────────────────────────┘
562  
563  lemma is_measurable_range_inr : is_measurable (range sum.inr : set (α ⊕ β)) :=
id                                   └───────────┘  └───┘ └─────┘   └─┘    
src                                  └───────────┘  └───┘ └─────┘   └─┘    
typ                                  └───────────┘  └───┘ └─────┘   └─┘    
doc                                  └───────────┘  └───┘
564  by rw [← image_univ]; exact is_measurable_inr_image is_measurable.univ
id            └────────┘         └─────────────────────┘ └────────────────┘
src     └────┘└────────┘  └────┘└─────────────────────┘└────────────────┘
typ     └────┘└────────┘  └────┘└─────────────────────┘└────────────────┘
doc     └────┘            └────┘                                         
txt     └────┘            └────┘                                         
par     └────┘            └────┘                                         
pid       └──┘                                                          
st     └───────────────┘└──────────────────────────────────────────────────
565  
src  
typ  
doc  
txt  
par  
pid  
st   
566  end sum
567  
568  instance {β : α → Type v} [m : Πa, measurable_space (β a)] : measurable_space (sigma β) :=
id                                    └──────────────┘        └──────────────┘  └───┘ 
src                                     └──────────────┘          └──────────────┘  └───┘
typ                                   └──────────────┘        └──────────────┘  └───┘ 
569  ⨅a, (m a).map (sigma.mk a)
id       └─┘   └──────┘ 
src         └─┘   └──────┘
typ      └─┘   └──────┘ 
doc         └─┘
570  
571  end constructions
572  
573  /-- Equivalences between measurable spaces. Main application is the simplification of measurability
574  statements along measurable equivalences. -/
575  structure measurable_equiv (α β : Type*) [measurable_space α] [measurable_space β] extends α ≃ β :=
id                                     └───┘   └──────────────┘    └──────────────┘             
src                                            └──────────────┘     └──────────────┘              
typ                                    └───┘   └──────────────┘    └──────────────┘             
doc                                                                                               
576  (measurable_to_fun : measurable to_fun)
id                        └────────┘ └────┘
src                       └────────┘
typ                       └────────┘ └────┘
doc                       └────────┘
577  (measurable_inv_fun : measurable inv_fun)
id                         └────────┘ └─────┘
src                        └────────┘
typ                        └────────┘ └─────┘
doc                        └────────┘
578  
579  
580  namespace measurable_equiv
581  
582  instance (α β) [measurable_space α] [measurable_space β] : has_coe_to_fun (measurable_equiv α β) :=
id                   └──────────────┘    └──────────────┘     └────────────┘  └──────────────┘  
src                  └──────────────┘     └──────────────┘      └────────────┘  └──────────────┘
typ                  └──────────────┘    └──────────────┘     └────────────┘  └──────────────┘  
doc                                                                             └──────────────┘
583  ⟨λ_, α → β, λe, e.to_equiv⟩
id               └───────┘
src                   └───────┘
typ              └───────┘
584  
585  lemma coe_eq {α β} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :
id                       └──────────────┘    └──────────────┘        └──────────────┘  
src                      └──────────────┘     └──────────────┘         └──────────────┘
typ                      └──────────────┘    └──────────────┘        └──────────────┘  
doc                                                                    └──────────────┘
586    (e : α → β) = e.to_equiv := rfl
id               └───────┘    └─┘
src                  └───────┘    └─┘
typ              └───────┘    └─┘
587  
588  def refl (α : Type*) [measurable_space α] : measurable_equiv α α :=
id                         └──────────────┘     └──────────────┘  
src                        └──────────────┘      └──────────────┘
typ                        └──────────────┘     └──────────────┘  
doc                                              └──────────────┘
589  { to_equiv := equiv.refl α,
id                 └────────┘ 
src                └────────┘
typ                └────────┘ 
590    measurable_to_fun := measurable_id, measurable_inv_fun := measurable_id }
id                          └───────────┘                        └───────────┘
src                         └───────────┘                        └───────────┘
typ                         └───────────┘                        └───────────┘
591  
592  def trans [measurable_space α] [measurable_space β] [measurable_space γ]
id              └──────────────┘    └──────────────┘    └──────────────┘ 
src             └──────────────┘     └──────────────┘     └──────────────┘
typ             └──────────────┘    └──────────────┘    └──────────────┘ 
593    (ab : measurable_equiv α β) (bc : measurable_equiv β γ) :
id           └──────────────┘          └──────────────┘  
src          └──────────────┘            └──────────────┘
typ          └──────────────┘          └──────────────┘  
doc          └──────────────┘            └──────────────┘
594    measurable_equiv α γ :=
id     └──────────────┘  
src    └──────────────┘
typ    └──────────────┘  
doc    └──────────────┘
595  { to_equiv := ab.to_equiv.trans bc.to_equiv,
id                 └┘└───────┘└────┘ └┘└───────┘
src                  └───────┘└────┘   └───────┘
typ                └┘└───────┘└────┘ └┘└───────┘
596    measurable_to_fun := bc.measurable_to_fun.comp ab.measurable_to_fun,
id                          └┘└────────────────┘└───┘ └┘└────────────────┘
src                           └────────────────┘└───┘   └────────────────┘
typ                         └┘└────────────────┘└───┘ └┘└────────────────┘
597    measurable_inv_fun := ab.measurable_inv_fun.comp bc.measurable_inv_fun }
id                           └┘└─────────────────┘└───┘ └┘└─────────────────┘
src                            └─────────────────┘└───┘   └─────────────────┘
typ                          └┘└─────────────────┘└───┘ └┘└─────────────────┘
598  
599  lemma trans_to_equiv {α β} [measurable_space α] [measurable_space β] [measurable_space γ]
id                               └──────────────┘    └──────────────┘    └──────────────┘ 
src                              └──────────────┘     └──────────────┘     └──────────────┘
typ                              └──────────────┘    └──────────────┘    └──────────────┘ 
600    (e : measurable_equiv α β) (f : measurable_equiv β γ) :
id          └──────────────┘         └──────────────┘  
src         └──────────────┘           └──────────────┘
typ         └──────────────┘         └──────────────┘  
doc         └──────────────┘           └──────────────┘
601    (e.trans f).to_equiv = e.to_equiv.trans f.to_equiv := rfl
id      └────┘  └──────┘   └───────┘└────┘ └───────┘    └─┘
src      └────┘   └──────┘    └───────┘└────┘  └───────┘    └─┘
typ     └────┘  └──────┘   └───────┘└────┘ └───────┘    └─┘
602  
603  def symm [measurable_space α] [measurable_space β] (ab : measurable_equiv α β) :
id             └──────────────┘    └──────────────┘         └──────────────┘  
src            └──────────────┘     └──────────────┘          └──────────────┘
typ            └──────────────┘    └──────────────┘         └──────────────┘  
doc                                                           └──────────────┘
604    measurable_equiv β α :=
id     └──────────────┘  
src    └──────────────┘
typ    └──────────────┘  
doc    └──────────────┘
605  { to_equiv := ab.to_equiv.symm,
id                 └┘└───────┘└───┘
src                  └───────┘└───┘
typ                └┘└───────┘└───┘
606    measurable_to_fun := ab.measurable_inv_fun,
id                          └┘└─────────────────┘
src                           └─────────────────┘
typ                         └┘└─────────────────┘
607    measurable_inv_fun := ab.measurable_to_fun }
id                           └┘└────────────────┘
src                            └────────────────┘
typ                          └┘└────────────────┘
608  
609  lemma symm_to_equiv {α β} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :
id                              └──────────────┘    └──────────────┘        └──────────────┘  
src                             └──────────────┘     └──────────────┘         └──────────────┘
typ                             └──────────────┘    └──────────────┘        └──────────────┘  
doc                                                                           └──────────────┘
610    e.symm.to_equiv = e.to_equiv.symm := rfl
id     └───┘└───────┘  └───────┘└───┘    └─┘
src     └───┘└───────┘   └───────┘└───┘    └─┘
typ    └───┘└───────┘  └───────┘└───┘    └─┘
611  
612  protected def cast {α β} [i₁ : measurable_space α] [i₂ : measurable_space β]
id                                  └──────────────┘         └──────────────┘ 
src                                 └──────────────┘          └──────────────┘
typ                                 └──────────────┘         └──────────────┘ 
613    (h : α = β) (hi : i₁ == i₂) : measurable_equiv α β :=
id                    └┘ └┘ └┘    └──────────────┘  
src                        └┘       └──────────────┘
typ                   └┘ └┘ └┘    └──────────────┘  
doc                                  └──────────────┘
614  { to_equiv := equiv.cast h,
id                 └────────┘ 
src                └────────┘
typ                └────────┘ 
615    measurable_to_fun  := by unfreezeI; subst h; subst hi; exact measurable_id,
id                                                       └┘        └───────────┘
src                             └───────┘  └────┘   └────┘    └────┘└───────────┘
typ                             └───────┘  └────┘  └────┘└┘  └────┘└───────────┘
doc                             └───────┘  └────┘   └────┘    └────┘
txt                             └───────┘  └────┘   └────┘    └────┘
par                             └───────┘  └────┘   └────┘    └────┘
pid                                                              
st                             └────────────────────────────────────────────────┘
616    measurable_inv_fun := by unfreezeI; subst h; subst hi; exact measurable_id }
id                                                       └┘        └───────────┘
src                             └───────┘  └────┘   └────┘    └────┘└───────────┘
typ                             └───────┘  └────┘  └────┘└┘  └────┘└───────────┘
doc                             └───────┘  └────┘   └────┘    └────┘             
txt                             └───────┘  └────┘   └────┘    └────┘             
par                             └───────┘  └────┘   └────┘    └────┘             
pid                                                                           
st                             └─────────────────────────────────────────────────┘
617  
618  protected lemma measurable {α β} [measurable_space α] [measurable_space β]
id                                     └──────────────┘    └──────────────┘ 
src                                    └──────────────┘     └──────────────┘
typ                                    └──────────────┘    └──────────────┘ 
619    (e : measurable_equiv α β) : measurable (e : α → β) :=
id          └──────────────┘      └────────┘        
src         └──────────────┘        └────────┘
typ         └──────────────┘      └────────┘        
doc         └──────────────┘        └────────┘
620  e.measurable_to_fun
id   └────────────────┘
src   └────────────────┘
typ  └────────────────┘
621  
622  protected lemma measurable_coe_iff {α β γ} [measurable_space α] [measurable_space β] [measurable_space γ]
id                                               └──────────────┘    └──────────────┘    └──────────────┘ 
src                                              └──────────────┘     └──────────────┘     └──────────────┘
typ                                              └──────────────┘    └──────────────┘    └──────────────┘ 
623    {f : β → γ} (e : measurable_equiv α β) : measurable (f ∘ e) ↔ measurable f :=
id                    └──────────────┘      └────────┘       └────────┘ 
src                     └──────────────┘        └────────┘         └────────┘
typ                   └──────────────┘      └────────┘       └────────┘ 
doc                     └──────────────┘        └────────┘           └────────┘
624  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
625    (assume hfe,
id             └─┘
typ            └─┘
626      have measurable (f ∘ (e.symm.trans e).to_equiv) := hfe.comp e.symm.measurable,
id            └────────┘     └───┘└────┘  └──────┘      └─┘└───┘ └───┘└─────────┘
src           └────────┘       └───┘└────┘   └──────┘         └───┘  └───┘└─────────┘
typ           └────────┘     └───┘└────┘  └──────┘      └─┘└───┘ └───┘└─────────┘
doc           └────────┘
627      by rwa [trans_to_equiv, symm_to_equiv, equiv.symm_trans] at this)
id               └────────────┘  └───────────┘  └──────────────┘
src         └───┘└────────────┘└┘└───────────┘└┘└──────────────┘└───────┘
typ         └───┘└────────────┘└┘└───────────┘└┘└──────────────┘└───────┘
doc         └───┘              └┘             └┘                └───────┘
txt         └───┘              └┘             └┘                └───────┘
par         └───┘              └┘             └┘                └───────┘
pid            └┘              └┘             └┘                └──────┘
st         └──────────────────┘└─────────────┘└────────────────┘└──────┘
628    (λh, h.comp e.measurable)
id         └───┘ └─────────┘
src          └───┘  └─────────┘
typ        └───┘ └─────────┘
629  
630  def prod_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ]
id                   └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘ 
src                  └──────────────┘     └──────────────┘     └──────────────┘     └──────────────┘
typ                  └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘ 
631    (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) :
id           └──────────────┘          └──────────────┘  
src          └──────────────┘            └──────────────┘
typ          └──────────────┘          └──────────────┘  
doc          └──────────────┘            └──────────────┘
632    measurable_equiv (α × γ) (β × δ) :=
id     └──────────────┘         
src    └──────────────┘           
typ    └──────────────┘         
doc    └──────────────┘
633  { to_equiv := equiv.prod_congr ab.to_equiv cd.to_equiv,
id                 └──────────────┘ └┘└───────┘ └┘└───────┘
src                └──────────────┘   └───────┘   └───────┘
typ                └──────────────┘ └┘└───────┘ └┘└───────┘
634    measurable_to_fun := measurable.prod_mk
id                          └────────────────┘
src                         └────────────────┘
typ                         └────────────────┘
635      (ab.measurable_to_fun.comp (measurable.fst measurable_id))
id        └┘└────────────────┘└───┘  └────────────┘ └───────────┘
src         └────────────────┘└───┘  └────────────┘ └───────────┘
typ       └┘└────────────────┘└───┘  └────────────┘ └───────────┘
636      (cd.measurable_to_fun.comp (measurable.snd measurable_id)),
id        └┘└────────────────┘└───┘  └────────────┘ └───────────┘
src         └────────────────┘└───┘  └────────────┘ └───────────┘
typ       └┘└────────────────┘└───┘  └────────────┘ └───────────┘
637    measurable_inv_fun := measurable.prod_mk
id                           └────────────────┘
src                          └────────────────┘
typ                          └────────────────┘
638      (ab.measurable_inv_fun.comp (measurable.fst measurable_id))
id        └┘└─────────────────┘└───┘  └────────────┘ └───────────┘
src         └─────────────────┘└───┘  └────────────┘ └───────────┘
typ       └┘└─────────────────┘└───┘  └────────────┘ └───────────┘
639      (cd.measurable_inv_fun.comp (measurable.snd measurable_id)) }
id        └┘└─────────────────┘└───┘  └────────────┘ └───────────┘
src         └─────────────────┘└───┘  └────────────┘ └───────────┘
typ       └┘└─────────────────┘└───┘  └────────────┘ └───────────┘
640  
641  def prod_comm [measurable_space α] [measurable_space β] : measurable_equiv (α × β) (β × α) :=
id                  └──────────────┘    └──────────────┘     └──────────────┘         
src                 └──────────────┘     └──────────────┘      └──────────────┘           
typ                 └──────────────┘    └──────────────┘     └──────────────┘         
doc                                                            └──────────────┘
642  { to_equiv := equiv.prod_comm α β,
id                 └─────────────┘  
src                └─────────────┘
typ                └─────────────┘  
643    measurable_to_fun  := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id),
id                           └────────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
src                          └────────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
typ                          └────────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
644    measurable_inv_fun := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id) }
id                           └────────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
src                          └────────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
typ                          └────────────────┘  └────────────┘ └───────────┘   └────────────┘ └───────────┘
645  
646  def sum_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ]
id                  └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘ 
src                 └──────────────┘     └──────────────┘     └──────────────┘     └──────────────┘
typ                 └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘ 
647    (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) :
id           └──────────────┘          └──────────────┘  
src          └──────────────┘            └──────────────┘
typ          └──────────────┘          └──────────────┘  
doc          └──────────────┘            └──────────────┘
648    measurable_equiv (α ⊕ γ) (β ⊕ δ) :=
id     └──────────────┘         
src    └──────────────┘           
typ    └──────────────┘         
doc    └──────────────┘
649  { to_equiv := equiv.sum_congr ab.to_equiv cd.to_equiv,
id                 └─────────────┘ └┘└───────┘ └┘└───────┘
src                └─────────────┘   └───────┘   └───────┘
typ                └─────────────┘ └┘└───────┘ └┘└───────┘
650    measurable_to_fun :=
651      begin
st       └─────
652        cases ab with ab' abm, cases ab', cases cd with cd' cdm, cases cd',
id               └┘                     └─┘        └┘                     └─┘
src        └────┘  └───────────┘  └────┘     └────┘  └───────────┘  └────┘
typ        └────┘└┘└───────────┘  └────┘└─┘  └────┘└┘└───────────┘  └────┘└─┘
doc        └────┘  └───────────┘  └────┘     └────┘  └───────────┘  └────┘
txt        └────┘  └───────────┘  └────┘     └────┘  └───────────┘  └────┘
par        └────┘  └───────────┘  └────┘     └────┘  └───────────┘  └────┘
pid               └───────────┘                   └───────────┘       
st   ──────────────────────────┘└─────────┘└─────────────────────┘└─────────┘└─
653        refine measurable_sum (measurable_inl.comp abm) (measurable_inr.comp cdm)
id                └────────────┘  └─────────────────┘ └─┘   └─────────────────┘ └─┘
src        └─────┘└────────────┘ └─────────────────┘   └┘ └─────────────────┘   └─
typ        └─────┘└────────────┘ └─────────────────┘└─┘└┘ └─────────────────┘└─┘└─
doc        └─────┘                                     └┘                       └─
txt        └─────┘                                     └┘                       └─
par        └─────┘                                     └┘                       └─
pid                                                   └┘                       
st   ────────────────────────────────────────────────────────────────────────────────
654      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
655    measurable_inv_fun :=
656      begin
st       └─────
657        cases ab with ab' _ abm, cases ab', cases cd with cd' _ cdm, cases cd',
id               └┘                       └─┘        └┘                       └─┘
src        └────┘  └─────────────┘  └────┘     └────┘  └─────────────┘  └────┘
typ        └────┘└┘└─────────────┘  └────┘└─┘  └────┘└┘└─────────────┘  └────┘└─┘
doc        └────┘  └─────────────┘  └────┘     └────┘  └─────────────┘  └────┘
txt        └────┘  └─────────────┘  └────┘     └────┘  └─────────────┘  └────┘
par        └────┘  └─────────────┘  └────┘     └────┘  └─────────────┘  └────┘
pid               └─────────────┘                   └─────────────┘       
st   ────────────────────────────┘└─────────┘└───────────────────────┘└─────────┘└─
658        refine measurable_sum (measurable_inl.comp abm) (measurable_inr.comp cdm)
id                └────────────┘  └─────────────────┘ └─┘   └─────────────────┘ └─┘
src        └─────┘└────────────┘ └─────────────────┘   └┘ └─────────────────┘   └─
typ        └─────┘└────────────┘ └─────────────────┘└─┘└┘ └─────────────────┘└─┘└─
doc        └─────┘                                     └┘                       └─
txt        └─────┘                                     └┘                       └─
par        └─────┘                                     └┘                       └─
pid                                                   └┘                       
st   ────────────────────────────────────────────────────────────────────────────────
659      end }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
660  
661  def set.prod [measurable_space α] [measurable_space β] (s : set α) (t : set β) :
id                 └──────────────┘    └──────────────┘        └─┘        └─┘ 
src                └──────────────┘     └──────────────┘         └─┘         └─┘
typ                └──────────────┘    └──────────────┘        └─┘        └─┘ 
662    measurable_equiv (set.prod s t) (s × t) :=
id     └──────────────┘  └──────┘       
src    └──────────────┘  └──────┘         
typ    └──────────────┘  └──────┘       
doc    └──────────────┘  └──────┘
663  { to_equiv := equiv.set.prod s t,
id                 └────────────┘  
src                └────────────┘
typ                └────────────┘  
664    measurable_to_fun := measurable.prod_mk
id                          └────────────────┘
src                         └────────────────┘
typ                         └────────────────┘
665      (measurable.subtype_mk $ measurable.fst $ measurable.subtype_val $ measurable_id)
id        └───────────────────┘   └────────────┘   └────────────────────┘   └───────────┘
src       └───────────────────┘   └────────────┘   └────────────────────┘   └───────────┘
typ       └───────────────────┘   └────────────┘   └────────────────────┘   └───────────┘
666      (measurable.subtype_mk $ measurable.snd $ measurable.subtype_val $ measurable_id),
id        └───────────────────┘   └────────────┘   └────────────────────┘   └───────────┘
src       └───────────────────┘   └────────────┘   └────────────────────┘   └───────────┘
typ       └───────────────────┘   └────────────┘   └────────────────────┘   └───────────┘
667    measurable_inv_fun := measurable.subtype_mk $ measurable.prod_mk
id                           └───────────────────┘   └────────────────┘
src                          └───────────────────┘   └────────────────┘
typ                          └───────────────────┘   └────────────────┘
668      (measurable.subtype_val $ measurable.fst $ measurable_id)
id        └────────────────────┘   └────────────┘   └───────────┘
src       └────────────────────┘   └────────────┘   └───────────┘
typ       └────────────────────┘   └────────────┘   └───────────┘
669      (measurable.subtype_val $ measurable.snd $ measurable_id) }
id        └────────────────────┘   └────────────┘   └───────────┘
src       └────────────────────┘   └────────────┘   └───────────┘
typ       └────────────────────┘   └────────────┘   └───────────┘
670  
671  def set.univ (α : Type*) [measurable_space α] : measurable_equiv (univ : set α) α :=
id                             └──────────────┘     └──────────────┘  └──┘   └─┘   
src                            └──────────────┘      └──────────────┘  └──┘   └─┘
typ                            └──────────────┘     └──────────────┘  └──┘   └─┘   
doc                                                  └──────────────┘
672  { to_equiv := equiv.set.univ α,
id                 └────────────┘ 
src                └────────────┘
typ                └────────────┘ 
673    measurable_to_fun := measurable.subtype_val measurable_id,
id                          └────────────────────┘ └───────────┘
src                         └────────────────────┘ └───────────┘
typ                         └────────────────────┘ └───────────┘
674    measurable_inv_fun := measurable.subtype_mk measurable_id }
id                           └───────────────────┘ └───────────┘
src                          └───────────────────┘ └───────────┘
typ                          └───────────────────┘ └───────────┘
675  
676  def set.singleton [measurable_space α] (a:α) : measurable_equiv ({a} : set α) unit :=
id                      └──────────────┘          └──────────────┘      └─┘   └──┘
src                     └──────────────┘            └──────────────┘       └─┘    └──┘
typ                     └──────────────┘          └──────────────┘      └─┘   └──┘
doc                                                 └──────────────┘               └──┘
677  { to_equiv := equiv.set.singleton a,
id                 └─────────────────┘ 
src                └─────────────────┘
typ                └─────────────────┘ 
678    measurable_to_fun := measurable_const,
id                          └──────────────┘
src                         └──────────────┘
typ                         └──────────────┘
679    measurable_inv_fun := measurable.subtype_mk $ show measurable (λu:unit, a), from
id                           └───────────────────┘        └────────┘     └──┘  
src                          └───────────────────┘        └────────┘     └──┘
typ                          └───────────────────┘        └────────┘     └──┘  
doc                                                       └────────┘     └──┘
680      measurable_const }
id       └──────────────┘
src      └──────────────┘
typ      └──────────────┘
681  
682  noncomputable def set.image [measurable_space α] [measurable_space β]
id                                └──────────────┘    └──────────────┘ 
src                               └──────────────┘     └──────────────┘
typ                               └──────────────┘    └──────────────┘ 
683    (f : α → β) (s : set α)
id                    └─┘ 
src                     └─┘
typ                   └─┘ 
684    (hf : function.injective f)
id           └────────────────┘ 
src          └────────────────┘
typ          └────────────────┘ 
685    (hfm : measurable f) (hfi : ∀s, is_measurable s → is_measurable (f '' s)) :
id            └────────┘             └───────────┘    └───────────┘   └┘ 
src           └────────┘               └───────────┘     └───────────┘    └┘
typ           └────────┘             └───────────┘    └───────────┘   └┘ 
doc           └────────┘               └───────────┘     └───────────┘
686    measurable_equiv s (f '' s) :=
id     └──────────────┘    └┘ 
src    └──────────────┘      └┘
typ    └──────────────┘    └┘ 
doc    └──────────────┘
687  { to_equiv := equiv.set.image f s hf,
id                 └─────────────┘   └┘
src                └─────────────┘
typ                └─────────────┘   └┘
688    measurable_to_fun  :=
689    begin
st     └─────
690      have : measurable (λa:s, f a) := hfm.comp (measurable.subtype_val measurable_id),
id              └────────┘              └──────┘  └────────────────────┘ └───────────┘
src      └─────┘└────────┘  └┘ └┘  └───┘└──────┘ └────────────────────┘└───────────┘
typ      └─────┘└────────┘  └┘└┘ └───┘└──────┘ └────────────────────┘└───────────┘
doc      └─────┘└────────┘  └┘ └┘  └───┘                                            
txt      └─────┘            └┘ └┘  └───┘                                            
par      └─────┘            └┘ └┘  └───┘                                            
pid      └───┘└┘            └┘ └┘  └──┘                                            
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
691      refine measurable.subtype_mk _,
id              └───────────────────┘
src      └─────┘└───────────────────┘└┘
typ      └─────┘└───────────────────┘└┘
doc      └─────┘                     └┘
txt      └─────┘                     └┘
par      └─────┘                     └┘
pid                                 └┘
st   ─────────────────────────────────┘└─
692      convert this,
id               └──┘
src      └──────┘
typ      └──────┘└──┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid             
st   ───────────────┘└─
693      ext ⟨a, h⟩, refl
src      └────────┘  └────
typ      └────────┘  └────
doc      └────────┘  └────
txt      └────────┘  └────
par      └────────┘  └────
pid         └─────┘      
st   ─────────────┘└──────
694    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
695    measurable_inv_fun :=
696      assume t ⟨u, (hu : is_measurable u), eq⟩,
id                        └───────────┘
src                         └───────────┘
typ                       └───────────┘
doc                         └───────────┘
697      begin
st       └─────
698        clear_, subst eq,
id                       └┘
src        └────┘  └────┘└┘
typ        └────┘  └────┘└┘
doc        └────┘  └────┘
txt        └────┘  └────┘
par        └────┘  └────┘
pid                     
st   ───────────┘└────────┘└─
699        show is_measurable {x : f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u},
id              └───────────┘       └┘       └─────────────┘   └┘                  
src        └───┘└───────────┘└──┘ └┘ └─┘  └─────────────┘    └────────┘ └────┘ 
typ        └───┘└───────────┘└──┘ └┘ └─┘  └─────────────┘└┘└────────┘ └────┘
doc        └───┘└───────────┘ └──┘    └─┘                     └────────┘ └────┘  
txt        └───┘              └──┘    └─┘                     └────────┘ └────┘  
par        └───┘              └──┘    └─┘                     └────────┘ └────┘  
pid        └───┘              └──┘    └─┘                     └────────┘ └────┘  
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
700        have : ∀(a ∈ s) (h : ∃a', a' ∈ s ∧ a' = a), classical.some h = a :=
id                                                 └────────────┘
src        └─────┘ └───┘ └─────┘└┘         └────────────┘   └───
typ        └─────┘ └───┘ └─────┘└┘        └────────────┘   └───
doc        └─────┘ └───┘ └─────┘ └┘                            └───
txt        └─────┘ └───┘ └─────┘ └┘                            └───
par        └─────┘ └───┘ └─────┘ └┘                            └───
pid        └───┘└┘ └───┘ └─────┘ └┘                            └───
st   ──────────────────────────────────────────────────────────────────────────
701          λa ha h, (classical.some_spec h).2,
id                     └─────────────────┘
src  ───────┘ └──────┘ └─────────────────┘ └─┘
typ  ───────┘ └──────┘ └─────────────────┘ └─┘
doc  ───────┘ └──────┘                     └─┘
txt  ───────┘ └──────┘                     └─┘
par  ───────┘ └──────┘                     └─┘
pid  ───────┘ └──────┘                     └┘
st   ─────────────────────────────────────────┘└─
702        rw show {x:f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u} = subtype.val ⁻¹' (f '' u),
id                              └─────────────┘    └┘                       └─────────┘ └─┘      
src        └─┘    └┘    └─┘  └─────────────┘    └────────┘ └────┘  └┘ └─────────┘└─┘     └──
typ        └─┘    └┘    └─┘  └─────────────┘ └┘└────────┘ └────┘  └┘└─────────┘└─┘   └──
doc        └─┘     └┘    └─┘                     └────────┘ └────┘  └┘            └─┘     └──
txt        └─┘     └┘    └─┘                     └────────┘ └────┘  └┘                    └──
par        └─┘     └┘    └─┘                     └────────┘ └────┘  └┘                    └──
pid               └┘    └─┘                     └────────┘ └────┘  └┘                    └──
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
703          by ext ⟨b, a, hbs, rfl⟩; simp [equiv.set.image, equiv.set.image_of_inj_on, hf, this _ hbs],
id                                          └─────────────┘  └───────────────────────┘  └┘  └──┘   └─┘
src  ──────────┘└──────────────────┘└┘└────┘└─────────────┘└┘└───────────────────────┘└┘  └┘    └─┘   
typ  ──────────┘└──────────────────┘└┘└────┘└─────────────┘└┘└───────────────────────┘└┘└┘└┘└──┘└─┘└─┘
doc  ──────────┘└──────────────────┘└┘└────┘               └┘                         └┘  └┘    └─┘   
txt  ──────────┘└──────────────────┘└┘└────┘               └┘                         └┘  └┘    └─┘   
par  ──────────┘└──────────────────┘└┘└────┘               └┘                         └┘  └┘    └─┘   
pid  ──────────────────────────────────────┘               └┘                         └┘  └┘    └─┘   
st   ─────────┘└──────────────────────────────────────────────────────────────────────────────────────┘└─
704        exact (measurable.subtype_val measurable_id) (f '' u) (hfi u hu)
id                └────────────────────┘ └───────────┘           └─┘  └┘
src        └────┘ └────────────────────┘└───────────┘└┘     └┘       └─
typ        └────┘ └────────────────────┘└───────────┘└┘    └┘ └─┘└┘└─
doc        └────┘                                    └┘     └┘       └─
txt        └────┘                                    └┘     └┘       └─
par        └────┘                                    └┘     └┘       └─
pid                                                 └┘     └┘       
st   ───────────────────────────────────────────────────────────────────────
705      end }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
706  
707  noncomputable def set.range [measurable_space α] [measurable_space β]
id                                └──────────────┘    └──────────────┘ 
src                               └──────────────┘     └──────────────┘
typ                               └──────────────┘    └──────────────┘ 
708    (f : α → β) (hf : function.injective f) (hfm : measurable f)
id                     └────────────────┘          └────────┘ 
src                      └────────────────┘           └────────┘
typ                    └────────────────┘          └────────┘ 
doc                                                   └────────┘
709    (hfi : ∀s, is_measurable s → is_measurable (f '' s)) :
id               └───────────┘    └───────────┘   └┘ 
src               └───────────┘     └───────────┘    └┘
typ              └───────────┘    └───────────┘   └┘ 
doc               └───────────┘     └───────────┘
710    measurable_equiv α (range f) :=
id     └──────────────┘   └───┘ 
src    └──────────────┘    └───┘
typ    └──────────────┘   └───┘ 
doc    └──────────────┘    └───┘
711  (measurable_equiv.set.univ _).symm.trans $
id    └───────────────────────┘   └──┘ └───┘
src   └───────────────────────┘   └──┘ └───┘
typ   └───────────────────────┘   └──┘ └───┘
712    (measurable_equiv.set.image f univ hf hfm hfi).trans $
id      └────────────────────────┘  └──┘ └┘ └─┘ └─┘ └───┘
src     └────────────────────────┘   └──┘            └───┘
typ     └────────────────────────┘  └──┘ └┘ └─┘ └─┘ └───┘
713    measurable_equiv.cast (by rw image_univ) (by rw image_univ)
id     └───────────────────┘        └────────┘         └────────┘
src    └───────────────────┘     └─┘└────────┘      └─┘└────────┘
typ    └───────────────────┘     └─┘└────────┘      └─┘└────────┘
doc                              └─┘                └─┘
txt                              └─┘                └─┘
par                              └─┘                └─┘
pid                                                  
st                              └────────────┘     └────────────┘
714  
715  def set.range_inl [measurable_space α] [measurable_space β] :
id                      └──────────────┘    └──────────────┘ 
src                     └──────────────┘     └──────────────┘
typ                     └──────────────┘    └──────────────┘ 
716    measurable_equiv (range sum.inl : set (α ⊕ β)) α :=
id     └──────────────┘  └───┘ └─────┘   └─┘       
src    └──────────────┘  └───┘ └─────┘   └─┘    
typ    └──────────────┘  └───┘ └─────┘   └─┘       
doc    └──────────────┘  └───┘
717  { to_fun    := λab, match ab with
id                   └┘        └┘
typ                  └┘        └┘
718      | ⟨sum.inl a, _⟩ := a
id          └─────┘ 
src         └─────┘
typ         └─────┘ 
719      | ⟨sum.inr b, p⟩ := have false, by cases p; contradiction, this.elim
id          └─────┘               └───┘                            └──┘└───┘
src         └─────┘               └───┘     └────┘   └───────────┘      └───┘
typ         └─────┘               └───┘     └────┘  └───────────┘  └──┘└───┘
doc                                         └────┘   └───────────┘
txt                                         └────┘   └───────────┘
par                                         └────┘   └───────────┘
pid                                              
st                                         └─────────────────────┘
720      end,
721    inv_fun   := λa, ⟨sum.inl a, a, rfl⟩,
id                      └─────┘     └─┘
src                      └─────┘       └─┘
typ                     └─────┘     └─┘
722    left_inv  := assume ⟨ab, a, eq⟩, by subst eq; refl,
id                                              └┘
src                                        └────┘└┘  └──┘
typ                                       └────┘└┘  └──┘
doc                                        └────┘    └──┘
txt                                        └────┘    └──┘
par                                        └────┘    └──┘
pid                                             
st                                        └─────────────┘
723    right_inv := assume a, rfl,
id                           └─┘
src                           └─┘
typ                          └─┘
724    measurable_to_fun  := assume s (hs : is_measurable s),
id                                         └───────────┘ 
src                                         └───────────┘
typ                                        └───────────┘ 
doc                                         └───────────┘
725      begin
st       └─────
726        refine ⟨_, is_measurable_inl_image hs, set.ext _⟩,
id                    └─────────────────────┘ └┘  └─────┘
src        └─────┘ └─┘└─────────────────────┘  └┘└─────┘└─┘
typ        └─────┘ └─┘└─────────────────────┘└┘└┘└─────┘└─┘
doc        └─────┘ └─┘                         └┘       └─┘
txt        └─────┘ └─┘                         └┘       └─┘
par        └─────┘ └─┘                         └┘       └─┘
pid               └─┘                         └┘       └─┘
st   ──────────────────────────────────────────────────────┘└─
727        rintros ⟨ab, a, rfl⟩,
src        └──────────────────┘
typ        └──────────────────┘
doc        └──────────────────┘
txt        └──────────────────┘
par        └──────────────────┘
pid               └───────────┘
st   ─────────────────────────┘└─
728        simp [set.range_inl._match_1]
id               └────────────────────┘
src        └────┘                      └─
typ        └────┘└────────────────────┘└─
doc        └────┘                      └─
txt        └────┘                      └─
par        └────┘                      └─
pid                                  
st   ────────────────────────────────────
729      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
730    measurable_inv_fun := measurable.subtype_mk measurable_inl }
id                           └───────────────────┘ └────────────┘
src                          └───────────────────┘ └────────────┘
typ                          └───────────────────┘ └────────────┘
731  
732  def set.range_inr [measurable_space α] [measurable_space β] :
id                      └──────────────┘    └──────────────┘ 
src                     └──────────────┘     └──────────────┘
typ                     └──────────────┘    └──────────────┘ 
733    measurable_equiv (range sum.inr : set (α ⊕ β)) β :=
id     └──────────────┘  └───┘ └─────┘   └─┘       
src    └──────────────┘  └───┘ └─────┘   └─┘    
typ    └──────────────┘  └───┘ └─────┘   └─┘       
doc    └──────────────┘  └───┘
734  { to_fun    := λab, match ab with
id                   └┘        └┘
typ                  └┘        └┘
735      | ⟨sum.inr b, _⟩ := b
id          └─────┘ 
src         └─────┘
typ         └─────┘ 
736      | ⟨sum.inl a, p⟩ := have false, by cases p; contradiction, this.elim
id          └─────┘               └───┘                            └──┘└───┘
src         └─────┘               └───┘     └────┘   └───────────┘      └───┘
typ         └─────┘               └───┘     └────┘  └───────────┘  └──┘└───┘
doc                                         └────┘   └───────────┘
txt                                         └────┘   └───────────┘
par                                         └────┘   └───────────┘
pid                                              
st                                         └─────────────────────┘
737      end,
738    inv_fun   := λb, ⟨sum.inr b, b, rfl⟩,
id                      └─────┘     └─┘
src                      └─────┘       └─┘
typ                     └─────┘     └─┘
739    left_inv  := assume ⟨ab, b, eq⟩, by subst eq; refl,
id                                              └┘
src                                        └────┘└┘  └──┘
typ                                       └────┘└┘  └──┘
doc                                        └────┘    └──┘
txt                                        └────┘    └──┘
par                                        └────┘    └──┘
pid                                             
st                                        └─────────────┘
740    right_inv := assume b, rfl,
id                           └─┘
src                           └─┘
typ                          └─┘
741    measurable_to_fun  := assume s (hs : is_measurable s),
id                                         └───────────┘ 
src                                         └───────────┘
typ                                        └───────────┘ 
doc                                         └───────────┘
742      begin
st       └─────
743        refine ⟨_, is_measurable_inr_image hs, set.ext _⟩,
id                    └─────────────────────┘ └┘  └─────┘
src        └─────┘ └─┘└─────────────────────┘  └┘└─────┘└─┘
typ        └─────┘ └─┘└─────────────────────┘└┘└┘└─────┘└─┘
doc        └─────┘ └─┘                         └┘       └─┘
txt        └─────┘ └─┘                         └┘       └─┘
par        └─────┘ └─┘                         └┘       └─┘
pid               └─┘                         └┘       └─┘
st   ──────────────────────────────────────────────────────┘└─
744        rintros ⟨ab, b, rfl⟩,
src        └──────────────────┘
typ        └──────────────────┘
doc        └──────────────────┘
txt        └──────────────────┘
par        └──────────────────┘
pid               └───────────┘
st   ─────────────────────────┘└─
745        simp [set.range_inr._match_1]
id               └────────────────────┘
src        └────┘                      └─
typ        └────┘└────────────────────┘└─
doc        └────┘                      └─
txt        └────┘                      └─
par        └────┘                      └─
pid                                  
st   ────────────────────────────────────
746      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
747    measurable_inv_fun := measurable.subtype_mk measurable_inr }
id                           └───────────────────┘ └────────────┘
src                          └───────────────────┘ └────────────┘
typ                          └───────────────────┘ └────────────┘
748  
749  def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
id                                 └──────────────┘    └──────────────┘    └──────────────┘ 
src                                └──────────────┘     └──────────────┘     └──────────────┘
typ                                └──────────────┘    └──────────────┘    └──────────────┘ 
750    measurable_equiv ((α ⊕ β) × γ) ((α × γ) ⊕ (β × γ)) :=
id     └──────────────┘                    
src    └──────────────┘                         
typ    └──────────────┘                    
doc    └──────────────┘
751  { to_equiv := equiv.sum_prod_distrib α β γ,
id                 └────────────────────┘   
src                └────────────────────┘
typ                └────────────────────┘   
752    measurable_to_fun  :=
753    begin
st     └─────
754      refine measurable_of_measurable_union_cover
id              └──────────────────────────────────┘
src      └─────┘└──────────────────────────────────┘
typ      └─────┘└──────────────────────────────────┘
doc      └─────┘                                    
txt      └─────┘                                    
par      └─────┘                                    
pid                                                
st   ────────────────────────────────────────────────
755        ((range sum.inl).prod univ)
id                 └─────┘
src  ─────┘       └─────┘└─────┘    └─
typ  ─────┘       └─────┘└─────┘    └─
doc  ─────┘              └─────┘    └─
txt  ─────┘              └─────┘    └─
par  ─────┘              └─────┘    └─
pid  ─────┘              └─────┘    └─
st   ──────────────────────────────────
756        ((range sum.inr).prod univ)
id           └───┘ └─────┘       └──┘
src  ─────┘  └───┘└─────┘└─────┘└──┘└─
typ  ─────┘  └───┘└─────┘└─────┘└──┘└─
doc  ─────┘  └───┘       └─────┘    └─
txt  ─────┘              └─────┘    └─
par  ─────┘              └─────┘    └─
pid  ─────┘              └─────┘    └─
st   ──────────────────────────────────
757        (is_measurable_set_prod is_measurable_range_inl is_measurable.univ)
id                                 └─────────────────────┘
src  ─────┘                       └─────────────────────┘                  └─
typ  ─────┘                       └─────────────────────┘                  └─
doc  ─────┘                                                                └─
txt  ─────┘                                                                └─
par  ─────┘                                                                └─
pid  ─────┘                                                                └─
st   ──────────────────────────────────────────────────────────────────────────
758        (is_measurable_set_prod is_measurable_range_inr is_measurable.univ)
id          └────────────────────┘ └─────────────────────┘ └────────────────┘
src  ─────┘ └────────────────────┘└─────────────────────┘└────────────────┘└─
typ  ─────┘ └────────────────────┘└─────────────────────┘└────────────────┘└─
doc  ─────┘                                                                └─
txt  ─────┘                                                                └─
par  ─────┘                                                                └─
pid  ─────┘                                                                └─
st   ──────────────────────────────────────────────────────────────────────────
759        (assume ⟨ab, c⟩ s, by cases ab; simp [set.prod_eq])
id                                     └┘        └─────────┘
src  ─────┘       └┘  └┘ └───┘  └────┘  └┘└────┘└─────────┘└─
typ  ─────┘       └┘  └┘ └───┘  └────┘└┘└┘└────┘└─────────┘└─
doc  ─────┘       └┘  └┘ └───┘  └────┘  └┘└────┘           └─
txt  ─────┘       └┘  └┘ └───┘  └────┘  └┘└────┘           └─
par  ─────┘       └┘  └┘ └───┘  └────┘  └┘└────┘           └─
pid  ─────┘       └┘  └┘ └───┘  └─────┘  └──────┘           └──
st   ──────────────────────────┘└───────────────────────────┘└─
760        _
src  ────────
typ  ────────
doc  ────────
txt  ────────
par  ────────
pid  ────────
st   ────────
761        _,
src  ──────┘
typ  ──────┘
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘└─
762      { refine (set.prod (range sum.inl) univ).symm.measurable_coe_iff.1 _,
id                 └──────┘  └───┘ └─────┘  └──┘
src        └─────┘ └──────┘ └───┘└─────┘└┘└──┘└───────────────────────────┘
typ        └─────┘ └──────┘ └───┘└─────┘└┘└──┘└───────────────────────────┘
doc        └─────┘          └───┘       └┘    └───────────────────────────┘
txt        └─────┘                      └┘    └───────────────────────────┘
par        └─────┘                      └┘    └───────────────────────────┘
pid                                    └┘    └───────────────────────────┘
st   ─────┘└────────────────────────────────────────────────────────────────┘└─
763        refine (prod_congr set.range_inl (set.univ _)).symm.measurable_coe_iff.1 _,
id                 └────────┘ └───────────┘  └──────┘
src        └─────┘ └────────┘└───────────┘ └──────┘└──────────────────────────────┘
typ        └─────┘ └────────┘└───────────┘ └──────┘└──────────────────────────────┘
doc        └─────┘                                 └──────────────────────────────┘
txt        └─────┘                                 └──────────────────────────────┘
par        └─────┘                                 └──────────────────────────────┘
pid                                               └──────────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
764        dsimp [(∘)],
id                
src        └─────┘└─┘
typ        └─────┘└─┘
doc        └─────┘ └─┘
txt        └─────┘ └─┘
par        └─────┘ └─┘
pid              └─┘
st   ────────────────┘└─
765        convert measurable_inl,
id                 └────────────┘
src        └──────┘└────────────┘
typ        └──────┘└────────────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid               
st   ───────────────────────────┘└─
766        ext ⟨a, c⟩, refl },
src        └────────┘  └───┘
typ        └────────┘  └───┘
doc        └────────┘  └───┘
txt        └────────┘  └───┘
par        └────────┘  └───┘
pid           └─────┘      
st   ───────────────┘└─────┘└┘
767      { refine (set.prod (range sum.inr) univ).symm.measurable_coe_iff.1 _,
id                 └──────┘  └───┘ └─────┘  └──┘
src        └─────┘ └──────┘ └───┘└─────┘└┘└──┘└───────────────────────────┘
typ        └─────┘ └──────┘ └───┘└─────┘└┘└──┘└───────────────────────────┘
doc        └─────┘          └───┘       └┘    └───────────────────────────┘
txt        └─────┘                      └┘    └───────────────────────────┘
par        └─────┘                      └┘    └───────────────────────────┘
pid                                    └┘    └───────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────┘└─
768        refine (prod_congr set.range_inr (set.univ _)).symm.measurable_coe_iff.1 _,
id                 └────────┘ └───────────┘  └──────┘
src        └─────┘ └────────┘└───────────┘ └──────┘└──────────────────────────────┘
typ        └─────┘ └────────┘└───────────┘ └──────┘└──────────────────────────────┘
doc        └─────┘                                 └──────────────────────────────┘
txt        └─────┘                                 └──────────────────────────────┘
par        └─────┘                                 └──────────────────────────────┘
pid                                               └──────────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
769        dsimp [(∘)],
id                
src        └─────┘└─┘
typ        └─────┘└─┘
doc        └─────┘ └─┘
txt        └─────┘ └─┘
par        └─────┘ └─┘
pid              └─┘
st   ────────────────┘└─
770        convert measurable_inr,
id                 └────────────┘
src        └──────┘└────────────┘
typ        └──────┘└────────────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid               
st   ───────────────────────────┘└─
771        ext ⟨b, c⟩, refl }
src        └────────┘  └───┘
typ        └────────┘  └───┘
doc        └────────┘  └───┘
txt        └────────┘  └───┘
par        └────────┘  └───┘
pid           └─────┘      
st   ───────────────┘└─────┘└─
772    end,
st   ────┘
773    measurable_inv_fun :=
774      begin
st       └─────
775        refine measurable_sum _ _,
id                └────────────┘
src        └─────┘└────────────┘└──┘
typ        └─────┘└────────────┘└──┘
doc        └─────┘              └──┘
txt        └─────┘              └──┘
par        └─────┘              └──┘
pid                            └──┘
st   ──────────────────────────────┘└─
776        { convert measurable.prod_mk
id                   └────────────────┘
src          └──────┘└────────────────┘
typ          └──────┘└────────────────┘
doc          └──────┘                  
txt          └──────┘                  
par          └──────┘                  
pid                                   
st   ───────┘└──────────────────────────
777            (measurable_inl.comp (measurable.fst measurable_id)) (measurable.snd measurable_id),
id              └─────────────────┘  └────────────┘                  └────────────┘ └───────────┘
src  ─────────┘ └─────────────────┘ └────────────┘             └─┘ └────────────┘└───────────┘
typ  ─────────┘ └─────────────────┘ └────────────┘             └─┘ └────────────┘└───────────┘
doc  ─────────┘                                                └─┘                            
txt  ─────────┘                                                └─┘                            
par  ─────────┘                                                └─┘                            
pid  ─────────┘                                                └─┘                            
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
778          ext ⟨a, c⟩; refl },
src          └────────┘  └───┘
typ          └────────┘  └───┘
doc          └────────┘  └───┘
txt          └────────┘  └───┘
par          └────────┘  └───┘
pid             └─────┘      
st   ────────────────────────┘└┘
779        { convert measurable.prod_mk
id                   └────────────────┘
src          └──────┘└────────────────┘
typ          └──────┘└────────────────┘
doc          └──────┘                  
txt          └──────┘                  
par          └──────┘                  
pid                                   
st   ───────────────────────────────────
780            (measurable_inr.comp (measurable.fst measurable_id)) (measurable.snd measurable_id),
id              └─────────────────┘  └────────────┘                  └────────────┘ └───────────┘
src  ─────────┘ └─────────────────┘ └────────────┘             └─┘ └────────────┘└───────────┘
typ  ─────────┘ └─────────────────┘ └────────────┘             └─┘ └────────────┘└───────────┘
doc  ─────────┘                                                └─┘                            
txt  ─────────┘                                                └─┘                            
par  ─────────┘                                                └─┘                            
pid  ─────────┘                                                └─┘                            
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
781          ext ⟨b, c⟩; refl }
src          └────────┘  └───┘
typ          └────────┘  └───┘
doc          └────────┘  └───┘
txt          └────────┘  └───┘
par          └────────┘  └───┘
pid             └─────┘      
st   ────────────────────────┘└─
782      end }
st   ──────┘
783  
784  def prod_sum_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
id                                 └──────────────┘    └──────────────┘    └──────────────┘ 
src                                └──────────────┘     └──────────────┘     └──────────────┘
typ                                └──────────────┘    └──────────────┘    └──────────────┘ 
785    measurable_equiv (α × (β ⊕ γ)) ((α × β) ⊕ (α × γ)) :=
id     └──────────────┘                    
src    └──────────────┘                         
typ    └──────────────┘                    
doc    └──────────────┘
786  prod_comm.trans $ (sum_prod_distrib _ _ _).trans $ sum_congr prod_comm prod_comm
id   └───────┘└────┘    └──────────────┘       └───┘    └───────┘ └───────┘ └───────┘
src  └───────┘└────┘    └──────────────┘       └───┘    └───────┘ └───────┘ └───────┘
typ  └───────┘└────┘    └──────────────┘       └───┘    └───────┘ └───────┘ └───────┘
787  
788  def sum_prod_sum (α β γ δ)
789    [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] :
id      └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘ 
src     └──────────────┘     └──────────────┘     └──────────────┘     └──────────────┘
typ     └──────────────┘    └──────────────┘    └──────────────┘    └──────────────┘ 
790    measurable_equiv ((α ⊕ β) × (γ ⊕ δ)) (((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ))) :=
id     └──────────────┘                                       
src    └──────────────┘                                                 
typ    └──────────────┘                                       
doc    └──────────────┘
791  (sum_prod_distrib _ _ _).trans $ sum_congr (prod_sum_distrib _ _ _) (prod_sum_distrib _ _ _)
id    └──────────────┘       └───┘    └───────┘  └──────────────┘         └──────────────┘
src   └──────────────┘       └───┘    └───────┘  └──────────────┘         └──────────────┘
typ   └──────────────┘       └───┘    └───────┘  └──────────────┘         └──────────────┘
792  
793  end measurable_equiv
794  
795  
796  namespace measurable_equiv
797  
798  end measurable_equiv
799  
800  namespace measurable_space
801  
802  /-- Dynkin systems
803  The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras generated
804  by intersection stable set systems.
805  -/
806  structure dynkin_system (α : Type*) :=
id                                └───┘
typ                               └───┘
807  (has : set α → Prop)
id          └─┘  
src         └─┘
typ         └─┘  
808  (has_empty : has ∅)
id                └─┘ 
src                   
typ               └─┘ 
809  (has_compl : ∀{a}, has a → has (-a))
id                    └─┘    └─┘  
src                                  
typ                   └─┘    └─┘  
810  (has_Union_nat : ∀{f:ℕ → set α}, pairwise (disjoint on f) → (∀i, has (f i)) → has (⋃i, f i))
id                         └─┘    └──────┘  └──────┘ └┘         └─┘        └─┘    
src                          └─┘     └──────┘  └──────┘ └┘                              
typ                        └─┘    └──────┘  └──────┘ └┘         └─┘        └─┘    
doc                                   └──────┘  └──────┘                                 
811  
812  theorem Union_decode2_disjoint_on
813    {β} [encodable β] {f : β → set α} (hd : pairwise (disjoint on f)) :
id          └───────┘           └─┘         └──────┘  └──────┘ └┘ 
src         └───────┘             └─┘          └──────┘  └──────┘ └┘
typ         └───────┘           └─┘         └──────┘  └──────┘ └┘ 
doc         └───────┘                          └──────┘  └──────┘
814    pairwise (disjoint on λ i, ⋃ b ∈ decode2 β i, f b) :=
id     └──────┘  └──────┘ └┘         └─────┘    
src    └──────┘  └──────┘ └┘           └─────┘    
typ    └──────┘  └──────┘ └┘         └─────┘    
doc    └──────┘  └──────┘                         
815  begin
st   └─────
816    rintro i j ij x ⟨h₁, h₂⟩,
src    └──────────────────────┘
typ    └──────────────────────┘
doc    └──────────────────────┘
txt    └──────────────────────┘
par    └──────────────────────┘
pid          └────────────────┘
st   ─────────────────────────┘└─
817    revert h₁ h₂,
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid          └────┘
st   ─────────────┘└─
818    simp, intros b₁ e₁ h₁ b₂ e₂ h₂,
src    └──┘  └──────────────────────┘
typ    └──┘  └──────────────────────┘
doc    └──┘  └──────────────────────┘
txt    └──┘  └──────────────────────┘
par    └──┘  └──────────────────────┘
pid                └────────────────┘
st   ─────┘└────────────────────────┘└─
819    refine hd _ _ _ ⟨h₁, h₂⟩,
id            └┘        └┘  └┘
src    └─────┘  └─────┘   └┘  
typ    └─────┘└┘└─────┘ └┘└┘└┘
doc    └─────┘  └─────┘   └┘  
txt    └─────┘  └─────┘   └┘  
par    └─────┘  └─────┘   └┘  
pid            └─────┘   └┘  
st   ─────────────────────────┘└─
820    cases encodable.mem_decode2.1 e₁,
id           └───────────────────┘   └┘
src    └────┘└───────────────────┘└─┘
typ    └────┘└───────────────────┘└─┘└┘
doc    └────┘                     └─┘
txt    └────┘                     └─┘
par    └────┘                     └─┘
pid                              └─┘
st   ─────────────────────────────────┘└─
821    cases encodable.mem_decode2.1 e₂,
id           └───────────────────┘   └┘
src    └────┘└───────────────────┘└─┘
typ    └────┘└───────────────────┘└─┘└┘
doc    └────┘                     └─┘
txt    └────┘                     └─┘
par    └────┘                     └─┘
pid                              └─┘
st   ─────────────────────────────────┘└─
822    exact mt (congr_arg _) ij
id           └┘  └───────┘    └┘
src    └────┘└┘ └───────┘└──┘  
typ    └────┘└┘ └───────┘└──┘└┘
doc    └────┘            └──┘  
txt    └────┘            └──┘  
par    └────┘            └──┘  
pid                     └──┘  
st   ───────────────────────────┘
823  end
st   └─┘
824  
825  namespace dynkin_system
826  
827  @[ext] lemma ext :
doc    └─┘
828    ∀{d₁ d₂ : dynkin_system α}, (∀s:set α, d₁.has s ↔ d₂.has s) → d₁ = d₂
id              └───────────┘       └─┘   └┘└──┘   └┘└──┘     └┘  └┘
src              └───────────┘         └─┘      └──┘      └──┘         
typ             └───────────┘       └─┘   └┘└──┘   └┘└──┘     └┘  └┘
doc              └───────────┘
829  | ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
id      └┘            └┘           
typ     └┘            └┘           
830    have s₁ = s₂, from funext $ assume x, propext $ h x,
id                       └────┘            └─────┘     
src                      └────┘             └─────┘
typ                      └────┘            └─────┘     
831    by subst this
id              └──┘
src       └────┘    
typ       └────┘└──┘
doc       └────┘    
txt       └────┘    
par       └────┘    
pid                
st       └───────────
832  
src  
typ  
doc  
txt  
par  
pid  
st   
833  variable (d : dynkin_system α)
id                 └───────────┘
src                └───────────┘
typ                └───────────┘
doc                └───────────┘
834  
835  lemma has_compl_iff {a} : d.has (-a) ↔ d.has a :=
id                             └──┘     └──┘ 
src                             └──┘       └──┘
typ                            └──┘     └──┘ 
836  ⟨λ h, by simpa using d.has_compl h, λ h, d.has_compl h⟩
id                       └─────────┘       └────────┘ 
src           └──────────┘└─────────┘         └────────┘
typ          └──────────┘└─────────┘      └────────┘ 
doc           └──────────┘           
txt           └──────────┘           
par           └──────────┘           
pid                └────┘           
st           └────────────────────────┘
837  
838  lemma has_univ : d.has univ :=
id                    └──┘ └──┘
src                    └──┘ └──┘
typ                   └──┘ └──┘
839  by simpa using d.has_compl d.has_empty
id                  └─────────┘ └─────────┘
src     └──────────┘└─────────┘└─────────┘
typ     └──────────┘└─────────┘└─────────┘
doc     └──────────┘                      
txt     └──────────┘                      
par     └──────────┘                      
pid          └────┘                      
st     └────────────────────────────────────
840  
src  
typ  
doc  
txt  
par  
pid  
st   
841  theorem has_Union {β} [encodable β] {f : β → set α}
id                          └───────┘           └─┘ 
src                         └───────┘             └─┘
typ                         └───────┘           └─┘ 
doc                         └───────┘
842    (hd : pairwise (disjoint on f)) (h : ∀i, d.has (f i)) : d.has (⋃i, f i) :=
id           └──────┘  └──────┘ └┘            └──┘        └──┘    
src          └──────┘  └──────┘ └┘               └──┘           └──┘   
typ          └──────┘  └──────┘ └┘            └──┘        └──┘    
doc          └──────┘  └──────┘                                        
843  by rw encodable.Union_decode2; exact
id         └─────────────────────┘
src     └─┘└─────────────────────┘  └────┘
typ     └─┘└─────────────────────┘  └────┘
doc     └─┘                         └────┘
txt     └─┘                         └────┘
par     └─┘                         └────┘
pid                                     
st     └──────────────────────────────────
844  d.has_Union_nat (Union_decode2_disjoint_on hd)
id   └─────────────┘  └───────────────────────┘ └┘
src  └─────────────┘ └───────────────────────┘  └─
typ  └─────────────┘ └───────────────────────┘└┘└─
doc                                             └─
txt                                             └─
par                                             └─
pid                                             └─
st   ───────────────────────────────────────────────
845    (λ n, encodable.Union_decode2_cases d.has_empty h)
id           └───────────────────────────┘ └─────────┘ 
src  ─┘  └──┘└───────────────────────────┘└─────────┘ └─
typ  ─┘  └──┘└───────────────────────────┘└─────────┘└─
doc  ─┘  └──┘                                         └─
txt  ─┘  └──┘                                         └─
par  ─┘  └──┘                                         └─
pid  ─┘  └──┘                                         
st   ─────────────────────────────────────────────────────
846  
src  
typ  
doc  
txt  
par  
pid  
st   
847  theorem has_union {s₁ s₂ : set α}
id                              └─┘ 
src                             └─┘
typ                             └─┘ 
848    (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₁ ∩ s₂ ⊆ ∅) : d.has (s₁ ∪ s₂) :=
id           └──┘ └┘        └──┘ └┘       └┘  └┘      └──┘  └┘  └┘
src           └──┘            └──┘                       └──┘     
typ          └──┘ └┘        └──┘ └┘       └┘  └┘      └──┘  └┘  └┘
849  by rw union_eq_Union; exact
id         └────────────┘
src     └─┘└────────────┘  └────┘
typ     └─┘└────────────┘  └────┘
doc     └─┘                └────┘
txt     └─┘                └────┘
par     └─┘                └────┘
pid                            
st     └─────────────────────────
850  d.has_Union (pairwise_disjoint_on_bool.2 h)
id   └─────────┘  └───────────────────────┘   
src  └─────────┘ └───────────────────────┘└─┘ └─
typ  └─────────┘ └───────────────────────┘└─┘└─
doc                                       └─┘ └─
txt                                       └─┘ └─
par                                       └─┘ └─
pid                                       └─┘ └─
st   ────────────────────────────────────────────
851    (bool.forall_bool.2 ⟨h₂, h₁⟩)
id      └──────────────┘    └┘  └┘
src  ─┘ └──────────────┘└─┘   └┘  └──
typ  ─┘ └──────────────┘└─┘ └┘└┘└┘└──
doc  ─┘                 └─┘   └┘  └──
txt  ─┘                 └─┘   └┘  └──
par  ─┘                 └─┘   └┘  └──
pid  ─┘                 └─┘   └┘  └┘
st   ────────────────────────────────
852  
src  
typ  
doc  
txt  
par  
pid  
st   
853  lemma has_diff {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ ⊆ s₁) : d.has (s₁ \ s₂) :=
id                           └─┘         └──┘ └┘        └──┘ └┘       └┘  └┘    └──┘  └┘  └┘
src                          └─┘           └──┘            └──┘                     └──┘     
typ                          └─┘         └──┘ └┘        └──┘ └┘       └┘  └┘    └──┘  └┘  └┘
854  d.has_compl_iff.1 begin
id   └────────────┘
src   └────────────┘
typ  └────────────┘
st                     └─────
855    simp [diff_eq, compl_inter],
id           └─────┘  └─────────┘
src    └────┘└─────┘└┘└─────────┘
typ    └────┘└─────┘└┘└─────────┘
doc    └────┘       └┘           
txt    └────┘       └┘           
par    └────┘       └┘           
pid               └┘           
st   ────────────────────────────┘└─
856    exact d.has_union (d.has_compl h₁) h₂ (λ x ⟨h₁, h₂⟩, h₁ (h h₂)),
id           └─────────┘  └─────────┘ └┘  └┘       └┘  └┘       
src    └────┘└─────────┘ └─────────┘  └┘    └──┘  └┘  └─┘      └┘
typ    └────┘└─────────┘ └─────────┘└┘└┘└┘  └──┘└┘└┘└┘└─┘     └┘
doc    └────┘                         └┘    └──┘  └┘  └─┘      └┘
txt    └────┘                         └┘    └──┘  └┘  └─┘      └┘
par    └────┘                         └┘    └──┘  └┘  └─┘      └┘
pid                                  └┘    └──┘  └┘  └─┘      └┘
st   ────────────────────────────────────────────────────────────────┘└─
857  end
st   ──┘
858  
859  instance : partial_order (dynkin_system α) :=
id              └───────────┘  └───────────┘ 
src             └───────────┘  └───────────┘
typ             └───────────┘  └───────────┘ 
doc                            └───────────┘
860  { le          := λm₁ m₂, m₁.has ≤ m₂.has,
id                    └┘ └┘  └┘└──┘  └┘└──┘
src                            └──┘    └──┘
typ                   └┘ └┘  └┘└──┘  └┘└──┘
861    le_refl     := assume a b, le_refl _,
id                              └─────┘
src                               └─────┘
typ                             └─────┘
862    le_trans    := assume a b c, le_trans,
id                               └──────┘
src                                 └──────┘
typ                              └──────┘
863    le_antisymm := assume a b h₁ h₂, ext $ assume s, ⟨h₁ s, h₂ s⟩ }
id                             └┘ └┘  └─┘             └┘   └┘ 
src                                     └─┘
typ                            └┘ └┘  └─┘             └┘   └┘ 
864  
865  def of_measurable_space (m : measurable_space α) : dynkin_system α :=
id                                └──────────────┘     └───────────┘ 
src                               └──────────────┘      └───────────┘
typ                               └──────────────┘     └───────────┘ 
doc                                                     └───────────┘
866  { has       := m.is_measurable,
id                  └────────────┘
src                  └────────────┘
typ                 └────────────┘
867    has_empty := m.is_measurable_empty,
id                  └──────────────────┘
src                  └──────────────────┘
typ                 └──────────────────┘
868    has_compl := m.is_measurable_compl,
id                  └──────────────────┘
src                  └──────────────────┘
typ                 └──────────────────┘
869    has_Union_nat := assume f _ hf, m.is_measurable_Union f hf }
id                               └┘  └──────────────────┘  └┘
src                                     └──────────────────┘
typ                              └┘  └──────────────────┘  └┘
870  
871  lemma of_measurable_space_le_of_measurable_space_iff {m₁ m₂ : measurable_space α} :
id                                                                 └──────────────┘ 
src                                                                └──────────────┘
typ                                                                └──────────────┘ 
872    of_measurable_space m₁ ≤ of_measurable_space m₂ ↔ m₁ ≤ m₂ :=
id     └─────────────────┘ └┘  └─────────────────┘ └┘  └┘  └┘
src    └─────────────────┘     └─────────────────┘        
typ    └─────────────────┘ └┘  └─────────────────┘ └┘  └┘  └┘
873  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
874  
875  /-- The least Dynkin system containing a collection of basic sets. -/
876  inductive generate_has (s : set (set α)) : set α → Prop
id                               └─┘  └─┘      └─┘
src                              └─┘  └─┘       └─┘
typ                              └─┘  └─┘      └─┘
877  | basic : ∀t∈s, generate_has t
id                               
typ                              
878  | empty : generate_has ∅
id                          
src                         
typ                         
879  | compl : ∀{a}, generate_has a → generate_has (-a)
id                  └──────────┘                  
src                                                 
typ                 └──────────┘                  
880  | Union : ∀{f:ℕ → set α}, pairwise (disjoint on f) →
id                   └─┘     └──────┘  └──────┘ └┘ 
src                   └─┘     └──────┘  └──────┘ └┘
typ                  └─┘     └──────┘  └──────┘ └┘ 
doc                            └──────┘  └──────┘
881      (∀i, generate_has (f i)) → generate_has (⋃i, f i)
id                                               
src                                                
typ                                              
doc                                                
882  
883  def generate (s : set (set α)) : dynkin_system α :=
id                     └─┘  └─┘      └───────────┘ 
src                    └─┘  └─┘       └───────────┘
typ                    └─┘  └─┘      └───────────┘ 
doc                                   └───────────┘
884  { has := generate_has s,
id            └──────────┘ 
src           └──────────┘
typ           └──────────┘ 
doc           └──────────┘
885    has_empty := generate_has.empty s,
id                  └────────────────┘ 
src                 └────────────────┘
typ                 └────────────────┘ 
886    has_compl := assume a, generate_has.compl,
id                           └────────────────┘
src                           └────────────────┘
typ                          └────────────────┘
887    has_Union_nat := assume f, generate_has.Union }
id                               └────────────────┘
src                               └────────────────┘
typ                              └────────────────┘
888  
889  instance : inhabited (dynkin_system α) := ⟨generate univ⟩
id              └───────┘  └───────────┘       └──────┘ └──┘
src             └───────┘  └───────────┘        └──────┘ └──┘
typ             └───────┘  └───────────┘       └──────┘ └──┘
doc                        └───────────┘
890  
891  def to_measurable_space (h_inter : ∀s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :=
id                                       └┘ └┘  └──┘ └┘   └──┘ └┘   └──┘  └┘  └┘
src                                              └──┘       └──┘       └──┘     
typ                                      └┘ └┘  └──┘ └┘   └──┘ └┘   └──┘  └┘  └┘
892  { measurable_space .
893    is_measurable := d.has,
id                      └──┘
src                      └──┘
typ                     └──┘
894    is_measurable_empty := d.has_empty,
id                            └────────┘
src                            └────────┘
typ                           └────────┘
895    is_measurable_compl := assume s h, d.has_compl h,
id                                      └────────┘ 
src                                        └────────┘
typ                                     └────────┘ 
896    is_measurable_Union := assume f hf,
id                                    └┘
typ                                   └┘
897      have ∀n, d.has (disjointed f n),
id               └──┘  └────────┘  
src                └──┘  └────────┘
typ              └──┘  └────────┘  
doc                      └────────┘
898        from assume n, disjointed_induct (hf n)
id                       └───────────────┘  └┘ 
src                       └───────────────┘
typ                      └───────────────┘  └┘ 
899          (assume t i h, h_inter _ _ h $ d.has_compl $ hf i),
id                       └─────┘        └────────┘   └┘ 
src                                          └────────┘
typ                      └─────┘        └────────┘   └┘ 
900      have d.has (⋃n, disjointed f n), from d.has_Union disjoint_disjointed this,
id            └──┘   └────────┘          └────────┘ └─────────────────┘ └──┘
src            └──┘    └────────┘             └────────┘ └─────────────────┘
typ           └──┘   └────────┘          └────────┘ └─────────────────┘ └──┘
doc                    └────────┘
901      by rwa [Union_disjointed] at this }
id               └──────────────┘
src         └───┘└──────────────┘└────────┘
typ         └───┘└──────────────┘└────────┘
doc         └───┘                └────────┘
txt         └───┘                └────────┘
par         └───┘                └────────┘
pid            └┘                └──────┘
st         └────────────────────┘└───────┘
902  
903  lemma of_measurable_space_to_measurable_space
904    (h_inter : ∀s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :
id                 └┘ └┘  └──┘ └┘   └──┘ └┘   └──┘  └┘  └┘
src                        └──┘       └──┘       └──┘     
typ                └┘ └┘  └──┘ └┘   └──┘ └┘   └──┘  └┘  └┘
905    of_measurable_space (d.to_measurable_space h_inter) = d :=
id     └─────────────────┘  └──────────────────┘ └─────┘   
src    └─────────────────┘   └──────────────────┘          
typ    └─────────────────┘  └──────────────────┘ └─────┘   
906  ext $ assume s, iff.rfl
id   └─┘            └─────┘
src  └─┘             └─────┘
typ  └─┘            └─────┘
907  
908  def restrict_on {s : set α} (h : d.has s) : dynkin_system α :=
id                        └─┘        └──┘     └───────────┘ 
src                       └─┘          └──┘      └───────────┘
typ                       └─┘        └──┘     └───────────┘ 
doc                                              └───────────┘
909  { has       := λt, d.has (t ∩ s),
id                     └──┘    
src                      └──┘    
typ                    └──┘    
910    has_empty := by simp [d.has_empty],
src                    └────┘           
typ                    └────┘└─────────┘
doc                    └────┘           
txt                    └────┘           
par                    └────┘           
pid                                   
st                    └─────────────────┘
911    has_compl := assume t hts,
id                          └─┘
typ                         └─┘
912      have -t ∩ s = (- (t ∩ s)) \ -s,
id                         
src                            
typ                        
913        from set.ext $ assume x, by by_cases x ∈ s; simp [h],
id              └─────┘                                  
src             └─────┘                └───────┘    └────┘ 
typ             └─────┘               └───────┘  └────┘
doc                                    └───────┘     └────┘ 
txt                                    └───────┘     └────┘ 
par                                    └───────┘     └────┘ 
pid                                                      
st                                    └───────────────────────┘
914      by rw [this]; from d.has_diff (d.has_compl hts) (d.has_compl h)
id              └──┘        └────────┘              └─┘   └─────────┘ 
src         └──┘      └───┘└────────┘               └┘ └─────────┘ └─
typ         └──┘└──┘  └───┘└────────┘            └─┘└┘ └─────────┘└─
doc         └──┘      └───┘                         └┘             └─
txt         └──┘      └───┘                         └┘             └─
par         └──┘      └───┘                         └┘             └─
pid           └┘      └───┘                         └┘             └─
st         └───────┘└───────────────────────────────────────────────────
915        (compl_subset_compl.mpr $ inter_subset_right _ _),
id          └────────────────────┘   └────────────────┘
src  ─────┘ └────────────────────┘ └────────────────┘└───┘
typ  ─────┘ └────────────────────┘ └────────────────┘└───┘
doc  ─────┘                                          └───┘
txt  ─────┘                                          └───┘
par  ─────┘                                          └───┘
pid  ─────┘                                          └───┘
st   ──────────────────────────────────────────────────────┘
916    has_Union_nat := assume f hd hf,
id                              └┘ └┘
typ                             └┘ └┘
917      begin
st       └─────
918        rw [inter_comm, inter_Union],
id             └────────┘  └─────────┘
src        └──┘└────────┘└┘└─────────┘
typ        └──┘└────────┘└┘└─────────┘
doc        └──┘          └┘           
txt        └──┘          └┘           
par        └──┘          └┘           
pid          └┘          └┘           
st   ───────────────────┘└───────────┘└──
919        apply d.has_Union_nat,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ──────────────────────────┘└─
920        { exact λ i j h x ⟨⟨_, h₁⟩, _, h₂⟩, hd i j h ⟨h₁, h₂⟩ },
id                                └┘      └┘   └┘
src          └────┘ └────────┘ └─┘  └────┘  └─┘        └┘  └┘
typ          └────┘ └────────┘ └─┘└┘└────┘└┘└─┘└┘      └┘  └┘
doc          └────┘ └────────┘ └─┘  └────┘  └─┘        └┘  └┘
txt          └────┘ └────────┘ └─┘  └────┘  └─┘        └┘  └┘
par          └────┘ └────────┘ └─┘  └────┘  └─┘        └┘  └┘
pid                └────────┘ └─┘  └────┘  └─┘        └┘  
st   ───────┘└──────────────────────────────────────────────────┘└┘
921        { simpa [inter_comm] using hf },
id                  └────────┘        └┘
src          └─────┘└────────┘└──────┘  
typ          └─────┘└────────┘└──────┘└┘
doc          └─────┘          └──────┘  
txt          └─────┘          └──────┘  
par          └─────┘          └──────┘  
pid                         └────┘  
st   ───────────────────────────────────┘└──
922      end }
st   ──────┘
923  
924  lemma generate_le {s : set (set α)} (h : ∀t∈s, d.has t) : generate s ≤ d :=
id                          └─┘  └─┘             └──┘     └──────┘   
src                         └─┘  └─┘                 └──┘      └──────┘   
typ                         └─┘  └─┘             └──┘     └──────┘   
925  λ t ht, ht.rec_on h d.has_empty
id      └┘  └┘└─────┘  └────────┘
src            └─────┘    └────────┘
typ     └┘  └┘└─────┘  └────────┘
926    (assume a _ h, d.has_compl h)
id                 └────────┘ 
src                    └────────┘
typ                └────────┘ 
927    (assume f hd _ hf, d.has_Union hd hf)
id              └┘  └┘  └────────┘ └┘ └┘
src                        └────────┘
typ             └┘  └┘  └────────┘ └┘ └┘
928  
929  lemma generate_inter {s : set (set α)}
id                             └─┘  └─┘ 
src                            └─┘  └─┘
typ                            └─┘  └─┘ 
930    (hs : ∀t₁ t₂ : set α, t₁ ∈ s → t₂ ∈ s → (t₁ ∩ t₂).nonempty → t₁ ∩ t₂ ∈ s) {t₁ t₂ : set α}
id                    └─┘   └┘     └┘      └┘  └┘ └──────┘    └┘  └┘             └─┘ 
src                   └─┘                            └──────┘                        └─┘
typ                   └─┘   └┘     └┘      └┘  └┘ └──────┘    └┘  └┘             └─┘ 
doc                                                     └──────┘
931    (ht₁ : (generate s).has t₁) (ht₂ : (generate s).has t₂) : (generate s).has (t₁ ∩ t₂) :=
id             └──────┘  └─┘  └┘          └──────┘  └─┘  └┘     └──────┘  └─┘   └┘  └┘
src            └──────┘   └─┘              └──────┘   └─┘         └──────┘   └─┘      
typ            └──────┘  └─┘  └┘          └──────┘  └─┘  └┘     └──────┘  └─┘   └┘  └┘
932  have generate s ≤ (generate s).restrict_on ht₂,
id        └──────┘    └──────┘  └─────────┘  └─┘
src       └──────┘     └──────┘   └─────────┘
typ       └──────┘    └──────┘  └─────────┘  └─┘
933    from generate_le _ $ assume s₁ hs₁,
id          └─────────┘            └┘ └─┘
src         └─────────┘
typ         └─────────┘            └┘ └─┘
934    have (generate s).has s₁, from generate_has.basic s₁ hs₁,
id           └──────┘  └─┘  └┘       └────────────────┘ └┘ └─┘
src          └──────┘   └─┘           └────────────────┘
typ          └──────┘  └─┘  └┘       └────────────────┘ └┘ └─┘
935    have generate s ≤ (generate s).restrict_on this,
id          └──────┘    └──────┘  └─────────┘  └──┘
src         └──────┘     └──────┘   └─────────┘
typ         └──────┘    └──────┘  └─────────┘  └──┘
936      from generate_le _ $ assume s₂ hs₂,
id            └─────────┘            └┘ └─┘
src           └─────────┘
typ           └─────────┘            └┘ └─┘
937        show (generate s).has (s₂ ∩ s₁), from
id               └──────┘  └─┘   └┘  └┘
src              └──────┘   └─┘      
typ              └──────┘  └─┘   └┘  └┘
938          (s₂ ∩ s₁).eq_empty_or_nonempty.elim
id            └┘  └┘ └──────────────────┘ └──┘
src                  └──────────────────┘ └──┘
typ           └┘  └┘ └──────────────────┘ └──┘
939          (λ h,  h.symm ▸ generate_has.empty _)
id                 └───┘  └────────────────┘
src                  └───┘  └────────────────┘
typ                └───┘  └────────────────┘
940          (λ h, generate_has.basic _ (hs _ _ hs₂ hs₁ h)),
id                └────────────────┘    └┘     └─┘ └─┘ 
src                └────────────────┘
typ               └────────────────┘    └┘     └─┘ └─┘ 
941    have (generate s).has (t₂ ∩ s₁), from this _ ht₂,
id           └──────┘  └─┘   └┘  └┘        └──┘   └─┘
src          └──────┘   └─┘      
typ          └──────┘  └─┘   └┘  └┘        └──┘   └─┘
942    show (generate s).has (s₁ ∩ t₂), by rwa [inter_comm],
id           └──────┘  └─┘   └┘  └┘           └────────┘
src          └──────┘   └─┘               └───┘└────────┘
typ          └──────┘  └─┘   └┘  └┘      └───┘└────────┘
doc                                        └───┘          
txt                                        └───┘          
par                                        └───┘          
pid                                           └┘          
st                                        └──────────────┘
943  this _ ht₁
id   └──┘   └─┘
typ  └──┘   └─┘
944  
945  lemma generate_from_eq {s : set (set α)}
id                               └─┘  └─┘ 
src                              └─┘  └─┘
typ                              └─┘  └─┘ 
946    (hs : ∀t₁ t₂ : set α, t₁ ∈ s → t₂ ∈ s → (t₁ ∩ t₂).nonempty → t₁ ∩ t₂ ∈ s) :
id                    └─┘   └┘     └┘      └┘  └┘ └──────┘    └┘  └┘  
src                   └─┘                            └──────┘           
typ                   └─┘   └┘     └┘      └┘  └┘ └──────┘    └┘  └┘  
doc                                                     └──────┘
947  generate_from s = (generate s).to_measurable_space (assume t₁ t₂, generate_inter hs) :=
id   └───────────┘    └──────┘  └─────────────────┘          └┘ └┘  └────────────┘ └┘
src  └───────────┘     └──────┘   └─────────────────┘                 └────────────┘
typ  └───────────┘    └──────┘  └─────────────────┘          └┘ └┘  └────────────┘ └┘
doc  └───────────┘
948  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
949    (generate_from_le $ assume t ht, generate_has.basic t ht)
id      └──────────────┘           └┘  └────────────────┘  └┘
src     └──────────────┘                └────────────────┘
typ     └──────────────┘           └┘  └────────────────┘  └┘
950    (of_measurable_space_le_of_measurable_space_iff.mp $
id      └────────────────────────────────────────────┘└─┘
src     └────────────────────────────────────────────┘└─┘
typ     └────────────────────────────────────────────┘└─┘
951      by rw [of_measurable_space_to_measurable_space];
id              └─────────────────────────────────────┘
src         └──┘└─────────────────────────────────────┘
typ         └──┘└─────────────────────────────────────┘
doc         └──┘                                       
txt         └──┘                                       
par         └──┘                                       
pid           └┘                                       
st         └──────────────────────────────────────────┘└─
952      from (generate_le _ $ assume t ht, is_measurable_generate_from ht))
id             └─────────┘                  └─────────────────────────┘
src      └───┘ └─────────┘└─┘       └─────┘└─────────────────────────┘  
typ      └───┘ └─────────┘└─┘       └─────┘└─────────────────────────┘  
doc      └───┘            └─┘       └─────┘                             
txt      └───┘            └─┘       └─────┘                             
par      └───┘            └─┘       └─────┘                             
pid      └───┘            └─┘       └─────┘                             
st   ─────────────────────────────────────────────────────────────────────┘
953  
954  end dynkin_system
955  
956  lemma induction_on_inter {C : set α → Prop} {s : set (set α)} {m : measurable_space α}
id                                 └─┘               └─┘  └─┘         └──────────────┘ 
src                                └─┘                └─┘  └─┘          └──────────────┘
typ                                └─┘               └─┘  └─┘         └──────────────┘ 
957    (h_eq : m = generate_from s)
id               └───────────┘ 
src               └───────────┘
typ              └───────────┘ 
doc                └───────────┘
958    (h_inter : ∀t₁ t₂ : set α, t₁ ∈ s → t₂ ∈ s → (t₁ ∩ t₂).nonempty → t₁ ∩ t₂ ∈ s)
id                         └─┘   └┘     └┘      └┘  └┘ └──────┘    └┘  └┘  
src                        └─┘                            └──────┘           
typ                        └─┘   └┘     └┘      └┘  └┘ └──────┘    └┘  └┘  
doc                                                          └──────┘
959    (h_empty : C ∅) (h_basic : ∀t∈s, C t) (h_compl : ∀t, m.is_measurable t → C t → C (- t))
id                                                   └────────────┘           
src                                                         └────────────┘              
typ                                                  └────────────┘           
960    (h_union : ∀f:ℕ → set α, (∀i j, i ≠ j → f i ∩ f j ⊆ ∅) →
id                     └─┘                   
src                     └─┘                            
typ                    └─┘                   
961      (∀i, m.is_measurable (f i)) → (∀i, C (f i)) → C (⋃i, f i)) :
id           └────────────┘                        
src            └────────────┘                              
typ          └────────────┘                        
doc                                                        
962    ∀{t}, m.is_measurable t → C t :=
id          └────────────┘     
src           └────────────┘
typ         └────────────┘     
963  have eq : m.is_measurable = dynkin_system.generate_has s,
id             └────────────┘  └────────────────────────┘ 
src             └────────────┘  └────────────────────────┘
typ            └────────────┘  └────────────────────────┘ 
doc                              └────────────────────────┘
964    by rw [h_eq, dynkin_system.generate_from_eq h_inter]; refl,
id            └──┘  └────────────────────────────┘ └─────┘
src       └──┘    └┘└────────────────────────────┘         └──┘
typ       └──┘└──┘└┘└────────────────────────────┘└─────┘  └──┘
doc       └──┘    └┘                                       └──┘
txt       └──┘    └┘                                       └──┘
par       └──┘    └┘                                       └──┘
pid         └┘    └┘                                     
st       └───────┘└──────────────────────────────────────┘└────┘
965  assume t ht,
id           └┘
typ          └┘
966  have dynkin_system.generate_has s t, by rwa [eq] at ht,
id        └────────────────────────┘            └┘
src       └────────────────────────┘         └───┘└┘└─────┘
typ       └────────────────────────┘       └───┘└┘└─────┘
doc       └────────────────────────┘         └───┘  └─────┘
txt                                          └───┘  └─────┘
par                                          └───┘  └─────┘
pid                                             └┘  └────┘
st                                          └──────┘└────┘
967  this.rec_on h_basic h_empty
id   └──┘└─────┘ └─────┘ └─────┘
src      └─────┘
typ  └──┘└─────┘ └─────┘ └─────┘
968    (assume t ht, h_compl t $ by rw [eq]; exact ht)
id              └┘  └─────┘           └┘         └┘
src                                 └──┘└┘  └────┘
typ             └┘  └─────┘       └──┘└┘  └────┘└┘
doc                                 └──┘    └────┘
txt                                 └──┘    └────┘
par                                 └──┘    └────┘
pid                                   └┘         
st                                 └─────┘└────────┘
969    (assume f hf ht, h_union f hf $ assume i, by rw [eq]; exact ht _)
id              └┘ └┘  └─────┘  └┘                   └┘         └┘
src                                                 └──┘└┘  └────┘  └┘
typ             └┘ └┘  └─────┘  └┘               └──┘└┘  └────┘└┘└┘
doc                                                 └──┘    └────┘  └┘
txt                                                 └──┘    └────┘  └┘
par                                                 └──┘    └────┘  └┘
pid                                                   └┘           └┘
st                                                 └─────┘└──────────┘
970  
971  end measurable_space